Vastly different solving times of 4.8.8 release builds for Windows, Linux, and macOS

[robby-phd]

For the following example, z3 4.8.8 gives a result instantaneously in Windows and macOS, but it somehow takes around 24 seconds in Linux.

(set-logic ALL)

(define-sort B () Bool)

(define-sort Z () Int)
(define-fun |Z.unary_-| ((x Z)) Z (- x))
(define-fun |Z.<=| ((x Z) (y Z)) B (<= x y))
(define-fun |Z.<| ((x Z) (y Z)) B (< x y))
(define-fun |Z.>| ((x Z) (y Z)) B (> x y))
(define-fun |Z.>=| ((x Z) (y Z)) B (>= x y))
(define-fun |Z.==| ((x Z) (y Z)) B (= x y))
(define-fun |Z.!=| ((x Z) (y Z)) B (not (= x y)))
(define-fun |Z.+| ((x Z) (y Z)) Z (+ x y))
(define-fun |Z.-| ((x Z) (y Z)) Z (- x y))
(define-fun |Z.*| ((x Z) (y Z)) Z (* x y))
(define-fun |Z./| ((x Z) (y Z)) Z (div x y))
(define-fun |Z.%| ((x Z) (y Z)) Z (rem x y))

(declare-sort ADT 0)
(declare-sort Type 0)
(declare-fun type-of (ADT) Type)
(declare-fun sub-type (Type Type) Bool)
(assert (forall ((x Type)) (sub-type x x)))
(assert (forall ((x Type) (y Type) (z Type)) (=> (and (sub-type x y) (sub-type y z)) (sub-type x z))))
(assert (forall ((x Type) (y Type)) (=> (and (sub-type x y) (sub-type y x)) (= x y))))
(declare-fun |ADT.==| (ADT ADT) B)

(assert (forall ((x ADT) (y ADT))
  (=> (|ADT.==| x y)
      (let ((t (type-of x)))
        (= t (type-of y))
          ))))

(declare-const cx!1 Z)
(declare-const |l:x| Z)
(declare-const cx!2 Z)
(declare-const cx!3 Z)
(declare-const |l:Res| Z)
(declare-const cx!4 Z)
(declare-const cx!5 Z)
(declare-const cx!9 Z)
(declare-const cx!10 B)

(declare-fun |.add| (Z Z) Z)

(assert (forall ((|l:x| Z) (|l:y| Z) (Res Z)) (=>
  (= Res (|.add| |l:x| |l:y|))
  (let ((cx!6 |l:x|))
  (let ((cx!7 |l:y|))
  (let ((cx!8 (|Z.+| cx!6 cx!7)))
    (and
      (= Res cx!8)))))
)))

(assert (= |l:x| cx!1))
(assert (and
  (= |l:x| cx!2)
  (= cx!3 (|Z.+| cx!2 1))
  (= |l:Res| cx!3)))
(assert (= |l:Res| cx!4))
(assert (= |l:x| cx!5))
(assert (= cx!9 (|.add| cx!5 1)))
(assert (= cx!10 (|Z.==| cx!4 cx!9)))
(assert (not cx!10))

(check-sat)
(exit)

[NikolajBjorner]

In the current builds I get exactly the same results

C:\z3\release>z3 4601.smt2 /st unsat (:added-eqs 125 :arith-assert-diseq 4598 :arith-assert-lower 4383 :arith-assert-upper 5902 :arith-assume-eqs 5 :arith-bound-prop 284 :arith-conflicts 5 :arith-eq-adapter 179 :arith-fixed-eqs 20 :arith-num-rows 100 :arith-offset-eqs 29 :arith-pivots 164 :arith-row-summations 1216 :arith-tableau-max-columns 232 :arith-tableau-max-rows 100 :binary-propagations 9447 :conflicts 12 :decisions 3903 :del-clause 145 :eliminated-vars 8 :final-checks 110 :interface-eqs 5 :max-generation 2 :max-memory 8.23 :memory 4.29 :mk-bool-var 525 :mk-clause 467 :num-allocs 278624308 :num-checks 1 :propagations 15339 :quant-instantiations 106 :restarts 105 :rlimit-count 1809708 :time 1.24 :total-time 1.25)

root@nikolaj-sl2:~/z3/build# ./z3 /mnt/c/z3/build/4601.smt2 -st unsat (:added-eqs 125 :arith-assert-diseq 4598 :arith-assert-lower 4383 :arith-assert-upper 5902 :arith-assume-eqs 5 :arith-bound-prop 284 :arith-conflicts 5 :arith-eq-adapter 179 :arith-fixed-eqs 20 :arith-num-rows 100 :arith-offset-eqs 29 :arith-pivots 164 :arith-row-summations 1216 :arith-tableau-max-columns 232 :arith-tableau-max-rows 100 :binary-propagations 9447 :conflicts 12 :decisions 3903 :del-clause 145 :eliminated-vars 8 :final-checks 110 :interface-eqs 5 :max-generation 2 :max-memory 8.17 :memory 4.25 :mk-bool-var 525 :mk-clause 467 :num-allocs 279479289 :num-checks 1 :propagations 15339 :quant-instantiations 106 :restarts 105 :rlimit-count 1809708 :time 3.66 :total-time 3.69)

[robby-phd]

Oh wow, this is way trickier than I thought. Anyway, below are the stats that I got.

(Btw, I first noticed the issue because CI testing is failing only in Linux because I put a timeout of 5 seconds: https://github.com/sireum/logika/actions/runs/186469543).

Windows 10 (VMWare Fusion on a macOS Catalina host)

C:\Temp
λ z3 /version
Z3 version 4.8.8 - 64 bit

C:\Temp                                  
λ z3 /st 4601.smt2                       
unsat                                    
(:added-eqs                 47           
 :arith-assert-diseq        877          
 :arith-assert-lower        1160         
 :arith-assert-upper        1260         
 :arith-assume-eqs          3            
 :arith-bound-prop          116          
 :arith-conflicts           5            
 :arith-eq-adapter          77           
 :arith-fixed-eqs           5            
 :arith-num-rows            38           
 :arith-offset-eqs          20           
 :arith-pivots              150          
 :arith-row-summations      743          
 :arith-tableau-max-columns 95           
 :arith-tableau-max-rows    38           
 :binary-propagations       2150         
 :conflicts                 6            
 :decisions                 1013         
 :del-clause                18           
 :eliminated-vars           8            
 :final-checks              53           
 :interface-eqs             3            
 :max-generation            1            
 :max-memory                5.75         
 :memory                    3.64         
 :mk-bool-var               247          
 :mk-clause                 198          
 :num-allocs                16778812     
 :num-checks                1            
 :propagations              2860         
 :quant-instantiations      51           
 :restarts                  50           
 :rlimit-count              375858       
 :time                      0.14         
 :total-time                0.14)

Ubuntu Linux 20.04 (VMWare Fusion on a macOS Catalina host)

➜  Temp z3 -version
Z3 version 4.8.8 - 64 bit

➜  Temp z3 -st 4601.smt2 
unsat
(:added-eqs                 6994
 :arith-assert-diseq        41092
 :arith-assert-lower        52413
 :arith-assert-upper        33473
 :arith-assume-eqs          14
 :arith-bound-prop          602
 :arith-conflicts           13
 :arith-eq-adapter          413
 :arith-fixed-eqs           3064
 :arith-num-rows            152
 :arith-offset-eqs          965
 :arith-pivots              568
 :arith-row-summations      3503
 :arith-tableau-max-columns 678
 :arith-tableau-max-rows    152
 :binary-propagations       77262
 :conflicts                 18
 :decisions                 7722
 :del-clause                362
 :eliminated-vars           8
 :final-checks              424
 :interface-eqs             14
 :max-generation            2
 :max-memory                47.38
 :memory                    17.58
 :mk-bool-var               1381
 :mk-clause                 1051
 :num-allocs                641932914313.00
 :num-checks                1
 :propagations              140020
 :quant-instantiations      411
 :restarts                  410
 :rlimit-count              48708908
 :time                      23.44
 :total-time                23.43)

macOS Catalina

➜  Temp z3 -version     
Z3 version 4.8.8 - 64 bit

➜  Temp z3 4601.smt2 -st
unsat
(:added-eqs                 47
 :arith-assert-diseq        877
 :arith-assert-lower        1160
 :arith-assert-upper        1260
 :arith-assume-eqs          3
 :arith-bound-prop          116
 :arith-conflicts           5
 :arith-eq-adapter          77
 :arith-fixed-eqs           5
 :arith-num-rows            38
 :arith-offset-eqs          20
 :arith-pivots              150
 :arith-row-summations      743
 :arith-tableau-max-columns 95
 :arith-tableau-max-rows    38
 :binary-propagations       2150
 :conflicts                 6
 :decisions                 1013
 :del-clause                18
 :eliminated-vars           8
 :final-checks              53
 :interface-eqs             3
 :max-generation            1
 :max-memory                5.82
 :memory                    3.76
 :mk-bool-var               247
 :mk-clause                 198
 :num-allocs                310079
 :num-checks                1
 :propagations              2860
 :quant-instantiations      51
 :restarts                  50
 :rlimit-count              375858
 :time                      0.14
 :total-time                0.15)

[logicReasoner]

@NikolajBjorner how do I print those statistics when using the C++ API?

[NikolajBjorner]

operator<< is overloaded for the "stats" class. So you can do:

s = solver(ctx)
s.add(....)
std::cout << s.check() << "\n";
std::cout << s.statistics() << "\n";