search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Consolidated bugs in arithmetic logics #4532

Closed wintered closed 3 years ago

wintered commented 4 years ago

The following trace shows a genuinely invalid model bug on a QF_NRA formula. 

[556] % z3-4.8.8 rewriter.flat=false model_validate=true small.smt2
sat
(model 
 (define-fun c () Real
  (/ 1.0 8.0))
 (define-fun b () Real
  1.0)
 (define-fun d () Real
  (/ 1.0 4096.0))
 (define-fun e () Real
  5.0)
 (define-fun a () Real
  (/ 2561.0 1024.0))
)
[557] % z3release rewriter.flat=false model_validate=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
(model 
 (define-fun e () Real
  (/ 9232379240400289791.0 4611686016279904256.0))
 (define-fun a () Real
  (- (/ 2143289343.0 2147483648.0)))
 (define-fun c () Real
  (/ 1.0 8.0))
 (define-fun d () Real
  (/ 50440315803061452800000000.0 631185189288030893469201889.0))
 (define-fun b () Real
  1.0)
)
[558] % 
[558] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (> (* d (+ (- 117.293372755 c) (* (- (- b 117.293372755) e) 
(* (- (- b) e) (- (- b) e))))) (+ e (* (- a e) (- a (* c (* c c)))))))
(assert (>= b 0))
(assert (> d 0))
(check-sat)
(get-model)
[559] %

OS: Ubuntu 18.04 Commit: 3b11493 Does not repro in 6ced699

muchang commented 4 years ago

(rewriter.flat=false) Refutation soundness bug on QF_LRA formula

[567] % z3-4.8.8 small.smt2
sat
[568] % z3release small.smt2
sat
[569] % z3release rewriter.flat=false small.smt2
unsat
[570] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Bool)
(declare-fun c () Real)
(assert (= 0 (ite (= (- a c) 1) 0 1)))
(assert (= (- a c) (ite b 0 1)))
(assert (= (/ 0 0) 1))
(check-sat)
[571] %

Commit: 07a1aea Does not repro in https://github.com/Z3Prover/z3/commit/6ced6995d00690f4f513622b3e2772895ed347f5

zhendongsu commented 4 years ago

Refutation soundness bug in arith.solver=6 (default mode): 

[521] % z3-4.8.8 small.smt2
sat
[522] % z3release smt.arith.solver=2 small.smt2
sat
[523] % z3release small.smt2
unsat
[524] % 
[524] % cat small.smt2
(set-logic ALL)
(declare-fun c (Int) Bool)
(declare-fun d (Int) Int)
(declare-fun e () Int)
(declare-fun f (Int Int Int) Int)
(assert (forall ((g Int)) (! (= (d g) (mod (d (to_int (/ 4 g))) 2)) :pattern ((c g)))))
(assert
 (exists ((h Int))
  (not
   (= (forall ((a Int) (b Int)) (= (f h a b) 0))
    (forall ((a Int)) (xor (> h 0 a) (= 0 (+ (ite (> h 1) e 0) (/ (d (- h)) 0)))))
    (>= 0 (mod 0 0))))))
(check-sat)
[525] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/274323b818b6217c4520b3a9c8eca2e509edfd0b Does not repro in 6ced699

zhendongsu commented 4 years ago

Another refutation unsoundness in arith.solver=6 with "purify-arith ctx-solver-simplify" tactics (its root cause is very likely the same as that for the preceding instance): 

[540] % z3release smt.arith.solver=2 small.smt2
unknown
sat
[541] % z3release smt.arith.solver=6 small.smt2
unsat
sat
[542] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun f () Real)
(assert (exists ((e Real)) (and (< 0 (div a (- b d))) (< (/ 0 0) 0))))
(assert (= (mod c f) b (+ d f)))
(check-sat-using (then purify-arith ctx-solver-simplify))
(check-sat)
[543] %

OS: Ubuntu 18.04 Commit: 274323b Does not repro in 6ced699

zhendongsu commented 4 years ago

Another likely related refutation unsoundness in arith.solver=6 (default mode and w/o quantifiers): 

[613] % z3release smt.arith.solver=2 small.smt2
sat
[614] % z3release smt.arith.solver=6 small.smt2
unsat
[615] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(assert (or (= c 0) (= d 1)))
(assert (= (+ d e) 0))
(assert (= (/ c a) 0 (* d e) (mod f b) b))
(check-sat)
[616] %

OS: Ubuntu 18.04 Commit: 274323b Does not repro in 6ced699

zhendongsu commented 4 years ago

A performance regression of arith.solver=6 vs. arith.solver=2: 

[595] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.025s
user    0m0.014s
sys     0m0.000s
[596] % 
[596] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[597] % 
[597] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (>= (* a (+ (mod (to_int c) 16) (* a (div (to_int b) (to_int (- 0.5)))))) (/ b 3200)))
(check-sat)
[598] %

OS: Ubuntu 18.04 Commit: 274323b

zhendongsu commented 4 years ago

Another performance regression instance of arith.solver=6 vs. arith.solver=2:

[535] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.015s
user    0m0.007s
sys     0m0.007s
[536] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[537] % 
[537] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> (div b (- a)) 1))
(assert (> (* c (- (* a b) 2)) a))
(assert (> c 0))
(assert (not (<= a (- 1) 1 b)))
(assert (>= b a))
(check-sat)
[538] %

OS: Ubuntu 18.04 Commit: 274323b Does not repro in https://github.com/Z3Prover/z3/commit/6ced6995d00690f4f513622b3e2772895ed347f5

zhendongsu commented 4 years ago

[UPDATED: No repro after 6524a70]

A genuinely invalid model bug (rewriter.flat=false, incremental instance): 

[548] % z3release model_validate=true rewriter.flat=false small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
(model 
  (define-fun b () Real
    (/ 39.0 256.0))
  (define-fun a () Real
    (/ 2048.0 529.0))
)
[549] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= (* (* 2 a) (* (- 1 b) b)) 1))
(push)
(check-sat)
(get-model)
[550] %

OS: Ubuntu 18.04 Commit: 274323b

levnach commented 4 years ago

The last bug is not reproduced in https://github.com/Z3Prover/z3/commit/6524a70c321075068caffc3bac6b463c1b3325e6

zhendongsu commented 4 years ago

The last bug is not reproduced in 6524a70

Yes, it seems so, Lev. I'll add another case that still reproduces.

zhendongsu commented 4 years ago

A genuinely invalid model bug (rewriter.flat=false, incremental instance):

[668] % z3release model_validate=true rewriter.flat=false small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
(model 
  (define-fun b () Real
    (/ 97.0 16.0))
  (define-fun a () Real
    (/ 1.0 4.0))
)
unsat
[669] % 
[669] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (> a 0))
(assert (>= b 6))
(push)
(assert (< (* (* 5 b) a (* 5 a)) 5))
(check-sat)
(get-model)

(reset)

(define-fun b () Real (/ 97.0 16.0))
(define-fun a () Real (/ 1.0 4.0))
(assert (> a 0))
(assert (>= b 6))
(push)
(assert (< (* (* 5 b) a (* 5 a)) 5))
(check-sat)
[670] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/6524a70c321075068caffc3bac6b463c1b3325e6 Does not repro in https://github.com/Z3Prover/z3/commit/6ced6995d00690f4f513622b3e2772895ed347f5

levnach commented 4 years ago

Something is wrong with encoding to monomials: Running z3 bug.smt2 model_validate=true rewriter.flat=false -tr:arith This is a part of .z3-trace -------- [arith] init_model ../../src/smt/theory_lra.cpp:3369 --------- number of constraints = 76 ... v4 j4 = 0.5 := a v5 j5 = 7 := b v6 t0 = 35 := ( 5.0 b) v7 t1 = 2.5 := ( 5.0 a) v8 j8 = 0.125 := ( a 5.0 a) v9 j9 = 4.375 := ( a 5.0 a 5.0 b) irr: v10 t2 = -2.375 := (+ ( a ( 5.0 a)) (* -5.0 a))

In italic there are two encodings that are incorrect. j8 should be equal to 0.5 5 0.5 = 1.25. The equality below does not hold either.

zhendongsu commented 4 years ago

An even simpler instance than the one in https://github.com/Z3Prover/z3/issues/4532#issuecomment-647032660 (hope it is of use): 

[556] % z3release rewriter.flat=false model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
(model 
  (define-fun a () Real
    (/ 1.0 2.0))
)
[557] % 
[557] % cat small.smt2
(declare-fun a () Real)
(push)
(assert (= (* a (* 2 a) (* 3 a)) 1))
(check-sat)
(get-model)
[558] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/02f34ea4b1ba339f58a940116891a2895e10cde0 Does not repro in https://github.com/Z3Prover/z3/commit/6ced6995d00690f4f513622b3e2772895ed347f5

zhendongsu commented 4 years ago

Another non-incremental instance to trigger a (genuinely) invalid model bug (the (set-logic AUFNIRA) is needed to trigger the bug): 

[775] % z3release model_validate=true rewriter.flat=false small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
(model 
  (define-fun b () Real
    (/ 1.0 4.0))
  (define-fun a () Real
    (/ 11.0 4.0))
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 3) (= x!1 1)) 3
      0))
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    (/ 23.0 8.0))
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 3) (= x!1 1)) 0
      1))
)
[776] % 
[776] % cat small.smt2
(set-logic AUFNIRA)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (> (div 3 (to_int (* b (* a 2)))) (/ (mod 1 (to_int (* a 2))) (/ b 2)) a 2))
(check-sat)
(get-model)
[777] %

OS: Ubuntu 18.04 Commit: 02f34ea

zhendongsu commented 4 years ago

A solution unsoundness (it could be the same as or related to the bugs in #2650, although nlsat.check_lemmas=true does not fail): 

[579] % z3release small.smt2
unsat
[580] % z3release rewriter.flat=false model_validate=true small.smt2
sat
[581] % z3release rewriter.flat=false model_validate=true nlsat.check_lemmas=true small.smt2
check lemma: !(25 x7 - 81 < 0)
check
check lemma: !(- x7 + x1^2 > 0)
check
check lemma: !(- x7 + x1^2 < 0)
check
check lemma: !(x5 > 0) or x5 = 0 or x7 + x3 x5 - x2 x5 = 0
check
check lemma: !(x5 > 0) or !(x3 x5 - x2 x5 + x1^2 > 0) or x5 = 0
check
check lemma: !(x1 < 0) or !(x3 - x2 < 0) or !(x3 - x2 + x1^2 > 0)
check
check lemma: !(x1 < 0) or !(25 x1^2 - 108 > 0)
check
check lemma: !(x5 > 0) or !(x3 x5 - x2 x5 + x1^2 < 0) or x5 = 0
check
check lemma: !(x0 < 0) or !(- x4 + x0^2 = 0) or x4 = 0 or - x9 + x3 x4 - x2 x4 = 0
check
sat
[582] %
[582] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(assert
 (not
  (exists ((i Real))
   (=> (<= (div b j) h)
    (< (+ (- a d) (/ (* (- b j) (- b j)) (* (- c e)))) 0.0 (- c e))
    (or (< f 0)
     (< (+ (* (+ (+ (* (* (- 1.0) (- c e)) (* g g)) (* (* 2.0 g) (- b j)) (- a d)))))
      f))))))
(assert (= c k))
(check-sat)
[583] %

OS: Ubuntu 18.04 Commit: 02f34ea

zhendongsu commented 4 years ago

A much simpler refutation soundness bug instance than the one in https://github.com/Z3Prover/z3/issues/4532#issuecomment-647014226: 

[581] % z3release smt.arith.solver=2 small.smt2
sat
[582] % z3release smt.arith.solver=6 small.smt2
unsat
[583] % cat small.smt2
(declare-fun a () Int)
(assert (= (/ (* 2 a) 0) (div 0 a) 1))
(check-sat)
[584] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/02f34ea4b1ba339f58a940116891a2895e10cde0 This fixed in https://github.com/Z3Prover/z3/commit/6ced6995d00690f4f513622b3e2772895ed347f5

NikolajBjorner commented 4 years ago

Seems to revolve around two bugs being addressed by: 6ced6995d00690f4f513622b3e2772895ed347f5 4b6ca6a10c318a9eb27f80304ce8aa05536cd4e1

zhendongsu commented 4 years ago

Seems to revolve around two bugs being addressed by: 6ced699 4b6ca6a

Nikolaj, we will double-check each of the instances and update accordingly; thanks.

NikolajBjorner commented 4 years ago

I have been double checking some, Lev others. The performance bugs are still open.

zhendongsu commented 4 years ago

I have been double checking some, Lev others. The performance bugs are still open.

Nikolaj, looks like all the above instances have been addressed by the three fixes by you and Lev; thanks.

zhendongsu commented 4 years ago

A performance regression of arith.solver=6 vs. arith.solver=2: 

[685] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.048s
user    0m0.013s
sys     0m0.004s
[686] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[687] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Real)
(declare-fun g () Bool)
(declare-fun h () Real)
(declare-fun i () Bool)
(declare-fun j () Real)
(assert
 (let ((k (* h)) (l (* f)))
  (and (or (and (or d (not b)) (or d (and (not b) (not e)))) (not c))
   (or (and (not b) (not e)) c)
   (or (and (= j 0) i (= a f 0)) (xor d true (not b)))
   (or g
    (and (<= 0 (+ (mod 10 a) (- (* h l) (- (- 1) (* h k)))))
     (or (> 0 (- (mod f (* 5 f)) a))
      (and (<= 8 a) (= (+ (mod 10 a) (+ (* h l) 1 (* h k))) 0)
       (<= (+ f h) 0) (= (> a 0) (> f 0)))))))))
(check-sat)
[688] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/5d36578684d239e2ebe75e8f5c490327c1cfef36

zhendongsu commented 4 years ago

A solution unsoundness (it might be the same as or related to the bugs in #2650, although nlsat.check_lemmas=true does not fail):

[580] % cvc4 -q small.smt2
unsat
[581] % z3release small.smt2
sat
[582] % 
[582] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(assert
 (not
  (exists ((u Real))
   (=>
    (and
     (=> (<= 0 u (/ (- (* (- 125.2833904241) e)) 557.1884422118))
      (and (>= (+ (* l u) r) 0)
       (<= (+ (* l u) r) p)
       (<= u t)))
     (<= r p)
     (> j (+ k (/ (* r r) (* 2 (/ a i)))))
     (> (/ a i) 0)
     (>= l 0)
     (> p 0)
     (> t 0))
    (<= (+ (* l (/ (- (- 125.2833904241 e)) 557.1884422118)) r) p)))))
(assert (= a (* i a m)(/ a i)))
(assert (= b (+ (*  125.2833904241 e) (* 557.1884422118 o)) f (/ c t) (/ c f) (* n l)))
(assert (= (/ b l) (+ (* g s) p h d q)))
(check-sat)
[583] %

OS: Ubuntu 18.04 Commit: 5d36578

NSB: basically 2650 related as it is within nlsat or nlqsat.

zhendongsu commented 4 years ago

A quite simple performance regression instance of arith.solver=6 vs. arith.solver=2: 

[549] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.212s
user    0m0.010s
sys     0m0.005s
[550] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[551] % 
[551] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (<= (/ a (* a a (+ a (mod (to_int a) (to_int a))))) 0 b))
(check-sat)
[552] %

OS: Ubuntu 18.04 Commit: 5d36578

zhendongsu commented 4 years ago

A solution unsoundness issue (appears to be a recent regression): 

[593] % z3-4.8.8 small.smt2
unsat
unsat
[594] % z3release small.smt2
sat
unsat
[595] % cat small.smt2
(set-logic QF_LIA)
(assert (or (= 0 1) (> 0 0)))
(check-sat-using (then sat-preprocess smt))
(check-sat)
[596] %

OS: Ubuntu 18.04 Commit: 5d36578 This one produces the incorrect "sat" when checking with (check-sat-using (then sat-preprocess smt)): by looking at the trace with "arith" I see that arith is not used.

zhendongsu commented 4 years ago

A refutation unsoundness in arith.solver=2:

[627] % z3release small.smt2
sat
[628] % z3release small.smt2 rewriter.flat=false smt.arith.solver=6
sat
[629] % z3release small.smt2 rewriter.flat=false smt.arith.solver=2
unsat
[630] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Int)
(assert (> (- a (* a (* a (- 1)))) b 1))
(check-sat)
[631] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/64f1a759a7fc550587aec313eabb11e0f4391f62

zhendongsu commented 4 years ago

A refutation unsoundness in arith.solver=6: 

[690] % z3release small.smt2
sat
[691] % z3release parallel.enable=true smt.threads=3 smt.arith.solver=2 small.smt2
sat
[692] % z3release parallel.enable=true smt.threads=3 smt.arith.solver=6 small.smt2
unsat
[693] % 
[693] % cat small.smt2
(set-logic QF_NIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(assert (= e (* f 56)))
(assert (= d (div e 68)))
(assert (= c (div d 33)))
(assert (= 2 (mod f 256) (mod c 256) (mod (mod (mod (mod (mod 0 a) 272) 72) b) 272)))
(check-sat)
[694] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/a29809132207db34aa486e1a916698cca360c6e9

zhendongsu commented 4 years ago

A refutation unsoundness in arith.solver=6 (e.g., <x=0, y=239> would be a model): 

[631] % z3release smt.arith.solver=2 small.smt2
sat
[632] % z3release smt.arith.solver=6 small.smt2
unsat
[633] % 
[633] % cat small.smt2
(set-option :unsat_core true)
(set-option :smt.phase_selection 0)
(set-option :smt.threads 3)
(set-option :smt.random_seed 16)
(set-option :parallel.enable true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (+ y (* 3 (+ 1 x y) x)) 239))
(check-sat)
[634] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/4d586c2c13b1a7af9c77c15c774c832cfe6edae0

NB: this is fixed FIXED in https://github.com/Z3Prover/z3/commit/8857a67e4f15607f0dc6f2311d62dae48ab55ec5

zhendongsu commented 4 years ago

A heap-use-after-free: 

[515] % z3release smt.arith.solver=6 small.smt2
sat
[516] % z3release rewriter.flat=false smt.arith.solver=2 small.smt2
unknown
[517] % z3release rewriter.flat=false smt.arith.solver=6 small.smt2
free(): invalid pointer
Aborted
[518] % z3san rewriter.flat=false smt.arith.solver=6 small.smt2
=================================================================
==20965==ERROR: AddressSanitizer: heap-use-after-free on address 0x62500021f4dc at pc 0x55fd78f6fd80 bp 0x7ffc67edd5e0 sp 0x7ffc67edd5d0
READ of size 4 at 0x62500021f4dc thread T0
    #0 0x55fd78f6fd7f in mpz_manager<false>::deallocate(bool, mpz_cell*) ../src/util/mpz.cpp:218
    #1 0x55fd78f717b2 in mpz_manager<false>::del(mpz_manager<false>*, mpz&) ../src/util/mpz.cpp:239
    #2 0x55fd78cfc02e in mpz_manager<false>::del(mpz&) ../src/util/mpz.h:406
    #3 0x55fd78cfc02e in mpq_manager<false>::del(mpz&) ../src/util/mpq.h:136
    #4 0x55fd78cfc02e in algebraic_numbers::manager::imp::del_poly(algebraic_numbers::algebraic_cell*) ../src/math/polynomial/algebraic_numbers.cpp:190
    #5 0x55fd78cfc02e in algebraic_numbers::manager::imp::del(algebraic_numbers::algebraic_cell*) ../src/math/polynomial/algebraic_numbers.cpp:201
    #6 0x55fd78cfc02e in algebraic_numbers::manager::imp::del(algebraic_numbers::anum&) ../src/math/polynomial/algebraic_numbers.cpp:212
    #7 0x55fd7872ef2d in arith_decl_plugin::algebraic_numbers_wrapper::recycle_id(unsigned int) ../src/ast/arith_decl_plugin.cpp:54
    #8 0x55fd7872ef2d in arith_decl_plugin::del(parameter const&) ../src/ast/arith_decl_plugin.cpp:112
    #9 0x55fd789af5bf in parameter::del_eh(ast_manager&, int) ../src/ast/ast.cpp:88
    #10 0x55fd789af5bf in decl_info::del_eh(ast_manager&) ../src/ast/ast.cpp:203
    #11 0x55fd789a7b73 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1955
    #12 0x55fd776fd850 in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1692
    #13 0x55fd776fd850 in ref_manager_wrapper<expr, ast_manager>::dec_ref(expr*) ../src/util/ref_vector.h:221
    #14 0x55fd776fd850 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_ref(expr*) ../src/util/ref_vector.h:36
    #15 0x55fd776fd850 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_range_ref(expr* const*, expr* const*) ../src/util/ref_vector.h:40
    #16 0x55fd776fd850 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::~ref_vector_core() ../src/util/ref_vector.h:61
    #17 0x55fd776fd850 in ref_vector<expr, ast_manager>::~ref_vector() ../src/util/ref_vector.h:232
    #18 0x55fd776fd850 in simple_factory<rational>::~simple_factory() ../src/model/value_factory.h:137
    #19 0x55fd776fd850 in numeral_factory::~numeral_factory() ../src/model/numeral_factory.h:28
    #20 0x55fd776fd850 in arith_factory::~arith_factory() ../src/model/numeral_factory.cpp:31
    ...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/util/mpz.cpp:218 in mpz_manager<false>::deallocate(bool, mpz_cell*)
...
==20965==ABORTING
[519] % 
[519] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun aa () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(assert (forall ((m Real)) (= f (/ m o))))
(assert
 (or
  (and
   (and
    (and
     (or
      (or
       (and
        (or
         (or
          (or
           (and
            (and
             (and
              (xor (< 0.0 (* ab i) (/ 7 b k))
               (and (and (< 0.0 (/ 77 (+ (* c ac) (- 2 ab)) aa)) (> (/ 7 aa) f))
                (<= i (/ 2 e f))))
              (<= 0.0 (* b k)))
             (distinct j 1.0))
            (< (- (/ 6 (- 10 a q) (* (+ 6 aa) (- 2.0 ad)))
                (/ (- 215 (- 216 (+ c ac)))
                 (+ 30 (+ (- (* c ac) (/ 10 203)) (/ f (- 51 e f)))
                  (* 131 (* 33 e f) aa)))) l))
           (<= 0.0 aa))
          (<= aa af))
         (>= (* (+ a q) (- 9 ad)) l))
        (= n 2.0))
       (>= 0 l))
      (>= 0.0 ad))
     (< 0.0 ae) (<= ae af c ac))
    (> 0.0 af))
   (> 0.0 (+ e f)))
  (>= 0.0 (* (/ 82 (* 2 c ac) (+ 7 b k)) aa) (/ 91 aa))))
(assert (distinct d h))
(assert (distinct g p))
(check-sat)
[520] %

OS: Ubuntu 18.04 Commit: 4d586c2

FIXED in https://github.com/Z3Prover/z3/commit/c7704ef9af37ffaf619311ea827bbcc00795fee8

zhendongsu commented 4 years ago

An invalid model bug by the sat-preprocess tactic (the bug is unrelated to arithmetic, but to https://github.com/Z3Prover/z3/issues/4532#issuecomment-648218012 in this thread, so it is also added to this thread): 

[524] % z3release model_validate=true small.smt2
sat
(error "line 4 column 31: an invalid model was generated")
(model 
  (define-fun a () Bool
    false)
  (define-fun b () Bool
    false)
)
[525] % 
[525] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (or a b))
(check-sat-using sat-preprocess)
(get-model)
[526] %

OS: Ubuntu 18.04 Commit: 4d586c2

FIXED in https://github.com/Z3Prover/z3/commit/ac39ddb43fd6a7126cdae85585ee94d7f5d81626

zhendongsu commented 4 years ago

A refutation unsoundness in arith.solver=6 (with the purify-arith and ctx-solver-simplify tactics): 

[643] % z3release smt.arith.solver=2 small.smt2
unknown
sat
[644] % z3release smt.arith.solver=6 small.smt2
unsat
sat
[645] %
[645] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ((d Real)) (exists ((e Real)) (and (=> true (=> (>= (* (/ (- 1) b) d d) c) (<= d a))) (> b 0)))))
(check-sat-using (then purify-arith ctx-solver-simplify))
(check-sat)
[646] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/2fb914d2a20a4ade2a4c8f7b71e5d0c5f67eb583

zhendongsu commented 4 years ago

A solution unsoundness (with the nnf and qffd tactics): 

[620] % z3release small.smt2
sat
unsat
[621] % 
[621] % cat small.smt2
(set-logic QF_LIA)
(declare-fun a () Bool)
(declare-fun b () Int)
(assert (= b (ite a 0 0)))
(assert (< 0 b 2))
(check-sat-using (then nnf qffd smt))
(check-sat)
[622] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/b71a64365d78618ae64083a99af2d1d6b90993d2

zhendongsu commented 4 years ago

A spurious invalid model error (as the generated model is in fact valid) by arith.solver=6: 

[510] % z3release model_validate=true smt.arith.solver=2 small.smt2
sat
(model 
  (define-fun f () Real
    (- 1.0))
  (define-fun b () Real
    0.0)
  (define-fun g () Real
    0.0)
  (define-fun d () Real
    (- 39.0))
  (define-fun a () Real
    0.0)
  (define-fun k () Real
    (- 1.0))
  (define-fun h () Real
    0.0)
  (define-fun e () Real
    (- 1.0))
  (define-fun c () Real
    0.0)
  (define-fun j () Real
    (- 1.0))
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    0)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    0)
)
[511] % z3release model_validate=true smt.arith.solver=6 small.smt2
sat
(error "line 18 column 40: an invalid model was generated")
(model 
  (define-fun f () Real
    1.0)
  (define-fun b () Real
    (- 1.0))
  (define-fun g () Real
    0.0)
  (define-fun d () Real
    (- 1.0))
  (define-fun a () Real
    0.0)
  (define-fun k () Real
    (- 2.0))
  (define-fun h () Real
    0.0)
  (define-fun e () Real
    (- 2.0))
  (define-fun j () Real
    1.0)
  (define-fun c () Real
    0.0)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    0)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    0)
)
[512] % 
[512] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(assert
 (forall ((i Real))
  (and (>= (div (to_int d) (to_int g)) 0)
   (xor (>= 0 a)
    (<= f 0 (mod (to_int j) (to_int i)) 0 k))
   (= c 0))))
(assert (= b (mod (to_int e) (to_int h))))
(check-sat-using (then purify-arith smt))
(get-model)
[513] %

OS: Ubuntu 18.04 Commit: 59d8895

zhendongsu commented 4 years ago

A refutation unsoundness bug in arith.solver=6:

[588] % z3release small.smt2
unsat
sat
[589] % cat small.smt2
(set-option :smt.phase_selection 6)
(set-option :smt.random_seed 18)
(set-option :rewriter.arith_lhs true)
(set-option :nlsat.shuffle_vars true)
(set-option :smt.arith.bprop_on_pivoted_rows false)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun f (Real) Real)
(assert (= (+ x x) 2))
(assert (= (* y y) 2 (* z z)))
(assert (distinct (f x) (f y)))
(assert (= (f x) (f z)))
(assert (distinct (f (/ x y)) (f (+ x z))))
(check-sat-using (then purify-arith ctx-solver-simplify qfbv))
(check-sat)
[590] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/02084dc95ba833ec94af8ba5ef2df132badd1fc0

zhendongsu commented 4 years ago

arith.solver=6 returns unknown on a simple regex instance (perhaps it should be filed under string logics?): 

[503] % z3release smt.arith.solver=2 small.smt2
sat
[504] % z3release smt.arith.solver=6 small.smt2
unknown
[505] % 
[505] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(assert (str.in_re (str.++ a c d) (re.union (str.to_re a) (str.to_re b))))
(check-sat)
[506] %

OS: Ubuntu 18.04 Commit: 02084dc

NikolajBjorner commented 4 years ago

this one isn't even a regular expression in the sense of a regular language because str.to_re arguments are variables and not string constants. The language for (re.++ (str.to_re a) (str.to_re a)) isn't regular. The cases where the solver will behave differently depending on random seeds are endless so I am not sure why it makes sense to file these as bugs. One can ask broadly what a semi-decision procedure for extended regular constraints may look like and then claim to solve it (simplest case is to bound lengths on a, b and compile away regex membership all-together), but it is better understood in context of a driving scenario.

zhendongsu commented 4 years ago

You're right, Nikolaj. Mentally and mistakenly, I placed quotes around the a's and b's, and viewed them as string constants.

muchang commented 4 years ago

Hi, for this QF_LIA formula, z3 gives an invalid model with qffd and qfufbv tactics:

[527] % z3release model_validate=true small.smt2
sat
(error "line 5 column 35: an invalid model was generated")
(model 
 ;; universe for (_ bv 1):
 ;;  bv!val!1 bv!val!0 
 ;; -----------
 ;; definitions for universe elements:
 (declare-fun bv!val!1 () (_ bv 1))
 (declare-fun bv!val!0 () (_ bv 1))
 ;; cardinality constraint:
 (forall ((x (_ bv 1))) (or (= x bv!val!1) (= x bv!val!0)))
 ;; -----------
 (define-fun bv () (_ bv 1)
  bv!val!1)
 (define-fun bv () (_ bv 1)
  bv!val!0)
 (define-fun b () Int
  1)
 (define-fun a () Int
  31)
)
[528] % 
[528] % cat small.smt2
(set-logic QF_UFLIA)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (and (or (= a 9) (= a 0)) (not (= 0 b))))
(check-sat-using (then qffd qfufbv))
(get-model)
[529] %

Commit: eef05e0

muchang commented 4 years ago

Here is another invalid model case with qffd and smt may be related to the above:

[529] % z3release model_validate=true small.smt2
sat
(error "line 9 column 32: an invalid model was generated")
(model
 ;; universe for (_ bv 4):
 ;;  bv!val!0 bv!val!1 bv!val!2
 ;; -----------
 ;; definitions for universe elements:
 (declare-fun bv!val!0 () (_ bv 4))
 (declare-fun bv!val!1 () (_ bv 4))
 (declare-fun bv!val!2 () (_ bv 4))
 ;; cardinality constraint:
 (forall ((x (_ bv 4))) (or (= x bv!val!0) (= x bv!val!1) (= x bv!val!2)))
 ;; -----------
 ;; universe for (_ bv 5):
 ;;  bv!val!1 bv!val!0
 ;; -----------
 ;; definitions for universe elements:
 (declare-fun bv!val!1 () (_ bv 5))
 (declare-fun bv!val!0 () (_ bv 5))
 ;; cardinality constraint:
 (forall ((x (_ bv 5))) (or (= x bv!val!1) (= x bv!val!0)))
 ;; -----------
 ;; universe for (_ bv 1):
 ;;  bv!val!0
 ;; -----------
 ;; definitions for universe elements:
 (declare-fun bv!val!0 () (_ bv 1))
 ;; cardinality constraint:
 (forall ((x (_ bv 1))) (= x bv!val!0))
 ;; -----------
 (define-fun c () Int
  3)
 (define-fun bv () (_ bv 1)
  bv!val!0)
 (define-fun bv () (_ bv 4)
  bv!val!1)
 (define-fun a () Int
  2)
 (define-fun b () Int
  2)
)
[530] %
[530] % cat small.smt2
(set-logic QF_UFLIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (distinct a b))
(assert (distinct a c))
(assert (<= 0 a 8))
(assert (<= 0 b 8))
(check-sat-using (then qffd smt))
(get-model)
[531] %

Commit: eef05e0

muchang commented 4 years ago

(nlsat.shuffle_vars=true, rewriter.flat=false) Soundness bug on QF_NRA formula with ctx-solver-simplify tactic.

[601] % z3release small.smt2
unsat
sat
[602] % cat small.smt2
(set-option :nlsat.shuffle_vars true)
(set-option :rewriter.flat false)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (>= (* a (- (* a (+ a 1)))) 1))
(assert (> (* b b) d))
(assert (= (* a a) (* c c) d))
(check-sat-using ctx-solver-simplify)
(check-sat)
[603] %

Commit: 7708874

muchang commented 4 years ago

(proof) Soundness bug on QF_LRA formula with ^

[504] % z3release small.smt2
sat
(model 
 (define-fun b () Real
  2.0)
 (define-fun a () Real
  0.0)
 (define-fun ^0 ((x!0 Real) (x!1 Real)) Real
  0.0)
)
[505] % 
[505] % z3release proof=true small.smt2
unsat
(error "line 5 column 10: model is not available")
[506] % 
[506] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (distinct b (^ a 0.0) 1.0))
(check-sat)
(get-model)
[507] %

Commit: 7708874

muchang commented 4 years ago

Soundness bug on QF_NRA formula with smt.random_seed=1.

[563] % z3release small.smt2
unsat
[564] % z3release smt.random_seed=1 small.smt2
sat
[565] %
[565] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun f () Real)
(declare-fun e () Real)
(declare-fun n () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun m () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(assert (not (exists ((i Real)) (not (=> (= i g) (<= d h))))))
(assert (not (forall ((l Real)) (=> (and (<= n 0.0 (- c n) j) (< (- b e) (- a f)) (< 0.0 k)) (or (< (- b e) (* 0.5 (+ (* m (- c n) (- c n)) (* 2.0 (- a f))))) (< (* (div (to_int (* (- m) (- c n))) (to_int j)) (/ (- m) (- c n))) (- b e)))))))
(assert (= c k))
(check-sat)
[566] %

Commit: 7708874

muchang commented 4 years ago

Segmentation fault(debug) and Assertion violation(release) on declare-datatypes with UFLIA logic.

[151] % z3release small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 432
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[152] % z3debug small.smt2 
Segmentation fault
[153] % z3asan small.smt2 
ASAN:DEADLYSIGNAL
=================================================================
==80881==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x56504aecfcf7 bp 0x7fff281d1b80 sp 0x7fff281d1b80 T0)
==80881==The signal is caused by a READ memory access.
==80881==Hint: address points to the zero page.
    #0 0x56504aecfcf6 in smt::theory_var_list::get_th_id() const ../src/smt/smt_theory_var_list.h:44
    #1 0x56504aecfcf6 in smt::enode::get_th_var(int) const ../src/smt/smt_enode.cpp:116
    #2 0x56504afcf674 in smt::theory_datatype::occurs_check_enter(smt::enode*) ../src/smt/theory_datatype.cpp:572
    #3 0x56504afd1857 in smt::theory_datatype::occurs_check(smt::enode*) ../src/smt/theory_datatype.cpp:655
    #4 0x56504afd3627 in smt::theory_datatype::final_check_eh() ../src/smt/theory_datatype.cpp:481
    #5 0x56504aa283dd in smt::context::final_check() ../src/smt/smt_context.cpp:3930
    #6 0x56504aa382ec in smt::context::bounded_search() ../src/smt/smt_context.cpp:3846
    #7 0x56504aa38be7 in smt::context::search() ../src/smt/smt_context.cpp:3670
    #8 0x56504aa3a7bb in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3553
    #9 0x56504aa87a0f in smt::model_checker::check(quantifier*) ../src/smt/smt_model_checker.cpp:340
    #10 0x56504aa88721 in smt::model_checker::check_quantifiers(bool&, unsigned int&) ../src/smt/smt_model_checker.cpp:486
    #11 0x56504aa88e0f in smt::model_checker::check(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_model_checker.cpp:432
    #12 0x56504a92a255 in smt::default_qm_plugin::check_model(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_quantifier.cpp:773
    #13 0x56504a92a255 in smt::quantifier_manager::imp::check_model(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_quantifier.cpp:421
    #14 0x56504a92a255 in smt::quantifier_manager::check_model(proto_model*, obj_map<smt::enode, app*> const&) ../src/smt/smt_quantifier.cpp:535
    #15 0x56504aa36fa5 in smt::context::restart(lbool&, unsigned int) ../src/smt/smt_context.cpp:3707
    #16 0x56504aa38c1e in smt::context::search() ../src/smt/smt_context.cpp:3675
    #17 0x56504aa3b363 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3493
    #18 0x56504a3b53ef in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
    #19 0x56504be5b925 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #20 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #21 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #22 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #23 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #24 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #25 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #26 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #27 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #28 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #29 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #30 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #31 0x56504be4e151 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
    #32 0x56504be5b925 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #33 0x56504be9579a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #34 0x56504be97a87 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
    #35 0x56504bcc8e38 in check_sat_core2 ../src/solver/tactic2solver.cpp:196
    #36 0x56504bd64e47 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #37 0x56504bd18f74 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:268
    #38 0x56504bd55031 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #39 0x56504bc678a8 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1553
    #40 0x56504bb84683 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #41 0x56504bb84683 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #42 0x56504bb84683 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #43 0x56504bb3ac55 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #44 0x565049163f96 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:115
    #45 0x5650490ff5de in main ../src/shell/main.cpp:363
    #46 0x7ff786bc4b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #47 0x565049113a79 in _start (/home/zhangche/reduce/z3asan+0x212a79)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/smt/smt_theory_var_list.h:44 in smt::theory_var_list::get_th_id() const
==80881==ABORTING
[154] % cat small.smt2 
(declare-datatypes ((a 0)) (((b))))
(declare-fun c (a Real) Real)
(assert (forall ((d a) (e Int)) (= (c d e) e)))
(assert (= 0 (c b 0)))
(check-sat)
[155] %

Commit: 7708874

muchang commented 4 years ago

(purify-arith, ctx-solver-simplify, nlsat.shuffle_vars) Soundness bug on NIRA formula

[587] % z3release small.smt2
unsat
sat
[588] % 
[588] % cat small.smt2
(set-option :nlsat.shuffle_vars true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun f () Real)
(assert
 (not
 (exists ((d Real))
  (let ((e a))
  (=> (=> (<= d c) (>= (+ b (* d d) (* d f)) 0))
   (>= c 0 a 0)
   (<= f (mod (to_int (* (- 10) a)) 5))
   (or (> (+ c a) 0) (= b (* f (+ c a)))))))))
(check-sat-using (then purify-arith ctx-solver-simplify))
(check-sat)
[589] %

OS: Ubuntu. 18.04 Commit: 5497538

muchang commented 4 years ago

(smt.threads=2) Refutation soundness bug on NIRA formula:

[558] % z3release small.smt2
sat
[559] % z3release smt.threads=2 small.smt2
unsat
[560] % 
[560] % cat small.smt2
(declare-fun k () Real)
(declare-fun a () Real)
(declare-fun c () Real)
(declare-fun b () Real)
(declare-fun l () Real)
(declare-fun e () Real)
(declare-fun d () Real)
(declare-fun m () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun n () Real)
(declare-fun f () Real)
(declare-fun j () Real)
(assert (not (exists ((i Real)) (=> (=> (<= i 0) (< i e)) (<= l m) (<= 0 h)))))
(assert (= k (* l n)))
(assert (= l (/ k n)))
(assert (= n (* k l) a (- e n)))
(assert (= e (/ a n)))
(assert (= n (/ a e) (/ n d)))
(assert (distinct c f))
(assert (= f (/ c m) 0))
(assert (= g (mod (to_int b) (to_int j)) (/ b g)))
(check-sat)
[561] %

OS: Ubuntu 18.04 Commit: 5497538

muchang commented 4 years ago

Regression segmentation fault with declare-datatypes

[621] % z3-4.8.8 small.smt2
sat
[622] % z3release small.smt2
Segmentation fault
[623] % 
[623] % cat small.smt2
(declare-datatypes ((k 0)) (((a (b k)) (dp))))
(declare-datatypes ((q 0)) (((r (c q)) (s))))
(declare-fun d () q)
(declare-fun l (k q) q)
(declare-sort o 0)
(declare-fun e (o) k)
(declare-fun f (o) q)
(declare-sort t 0)
(declare-fun m (t) k)
(declare-sort g 0)
(declare-fun h (g) q)
(assert (forall ((i o)) (and (= (l (e i) (f i)) (ite ((_ is s) (f i))
  s (ite ((_ is dp) (e i)) (f i) (ite (and ((_ is a) (e i))) (l (b (e
  i)) (c (f i))) d)))) (ite ((_ is s) (f i)) true (ite ((_ is dp) (e
  i)) true (ite (and ((_ is r) (f i))) (not (forall ((p o)) (not (and
  (= (e p) (b (e i))))))) true))))))
(assert (forall ((i g)) (and (ite ((_ is s) (h i)) true (ite ((_ is r)
  (h i)) (not (forall ((p g)) (not (= (h p) (c (h i)))))) true)))))
(assert (exists ((j k) (n q)) (not (and (forall ((p o)) (not (and (=
  (e p) j)))) (forall ((p t)) (not (and (= (m p) j)))) (forall ((p
  g)) (not (= (h p) n)))))))
(check-sat)
[624] %

OS: Ubuntu 18.04 Commit: ba5c9c3

muchang commented 4 years ago

Z3san stack overflow on QF_S formula

[521] % timeout -s 9 30 z3release small.smt2
Killed
[522] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==2740==ERROR: AddressSanitizer: stack-overflow on address 0x7fff90e1e3d8 (pc 0x55e9dcf9c905 bp 0x7fff90e1f2c0 sp 0x7fff90e1e380 T0)
  #0 0x55e9dcf9c904 in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2911
  #1 0x55e9dcf9c796 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2545
  #2 0x55e9dcf9d18d in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2922
  #3 0x55e9dcf9c796 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2545
...
SUMMARY: AddressSanitizer: stack-overflow ../src/ast/rewriter/seq_rewriter.cpp:2911 in seq_rewriter::mk_derivative_rec(expr*, expr*)
==2740==ABORTING
[523] % 
[523] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun g () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun h () String)
(assert (= "escapex3e" c))
(assert (= "escapex3cescapex2fescapex74escapex65escapex78escapex74escapex61escapex72escapex65escapex3eescapex0descapex0a" d))
(assert (= (str.++ c a d) g))
(assert (= e "escapex3cescapex73escapex65escapex6cescapex65escapex63escapex74escapex20escapex6eescapex61escapex6descapex65escapex3descapex27escapex62escapex62escapex63escapex6fescapex6cescapex6fescapex6cescapex65escapex3descapex27escapex77escapex69escapex64escapex74escapex68escapex3aescapex39escapex30escapex70escapex78escapex3bescapex27escapex20escapex6fescapex6eescapex43escapex68escapex61escapex74escapex28escapex27escapex6descapex65escapex73escapex73escapex61escapex67escapex65escapex27escapex2cescapex20escapex27escapex5bescapex63escapex6fescapex6cescapex6fescapex72escapex3descapex27escapex20escapex2bescapex20escapex74escapex68escapex69escapex73escapex2eescapex6fescapex70escapex74escapex75escapex65escapex3descapex27escapex6descapex61escapex72escapex6fescapex6fescapex6eescapex27escapex20escapex73escapex74escapex79escapex6cescapex65escapex3descapex27escapex63escapex6fescapex6cescapex6fescapex72escapex3aescapex6descapex61escapex72escapex6fescapex6fescapex6eescapex3bescapex27escapex3eescapex4descapex61escapex72escapex6fescapex6fescapex6eescapex3cescapex2fescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex3eescapex0descapex0aescapex3cescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex20escapex76escapex61escapex6cescapex75escapex65escapex3descapex27escapex72escapex65escapex64escapex27escapex20escapex73escapex74escapex79escapex6cescapex65escapex3descapex27escapex63escapex6fescapex6cescapex6fescapex72escapex3aescapex72escapex65escapex64escapex3bescapex27escapex3eescapex52escapex65escapex64escapex3cescapex2fescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex3eescapex0descapex0aescapex3cescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex20escapex76escapex61escapex6cescapex75escapex65escapex3descapex27escapex6fescapex72escapex61escapex6eescapex67escapex65escapex27escapex20escapex73escapex74escapex79escapex6cescapex65escaescapex62escapex6cescapex32escapex27escapex3eescapex0descapex0a"))
(assert (= (str.++ g e) f))
(assert (= h (str.++ f b)))
(assert (str.in_re h (re.++ (re.* re.allchar) (str.to_re "escapex5c") (re.* re.allchar))))
(check-sat)
[524] %

OS: Ubuntu 18.04 Commit: ba5c9c3

muchang commented 4 years ago

Segmentation fault with declare-datatypes (might be the same as https://github.com/Z3Prover/z3/issues/4532#issuecomment-696043836)

[553] % z3-4.8.8 small.smt2
unsat
[554] % z3release small.smt2
Segmentation fault
[555] % 
[555] % cat small.smt2
(declare-datatypes ((T 0)) (((a))))
(declare-fun b (T) Real)
(assert (forall ((c T) (d Int)) (= (b c) d)))
(assert (forall ((e Int)) (= e 0)))
(check-sat)
[556] %

OS: Ubuntu 18.04 Commit: 1e6d2fb

muchang commented 4 years ago

(model_evaluator.array_equalities=false, rewriter.flat=false) Refutation soundness bug on LIA formula

[171] % z3release small.smt2
unsat
[172] % cvc4 -q small.smt2 
unsupported
unsupported
sat
[173] % ./z3-4.8.5-x64-ubuntu-16.04/bin/z3 small.smt2 
sat
[174] % cat small.smt2 
(set-option :model_evaluator.array_equalities false)       
(set-option :rewriter.flat false)       
(declare-fun a () Bool)      
(assert (forall ((b Int)(c Int)(d Int)(g Int)) 
  (let (($e (and (>= d c) (not (<= c g)))) ($f (or a (= 5 b))))     
  (let (($d (or (not $f) (= d g)))) (not (and $d $e))))))
(check-sat)                                                                
[175] %

OS: Ubuntu 18.04 Commit: 79162b9

muchang commented 4 years ago

z3 arith.solver=6 performance regression vs. arith.solver=2 on QF_NIRA formula

[558] % time cvc4 -q small.smt2
sat
real  0m0.115s
user  0m0.016s
sys   0m0.006s
[559] % time z3-4.8.8 smt.arith.solver=2 small.smt2
sat
real  0m0.056s
user  0m0.008s
sys   0m0.008s
[560] % time z3-4.8.8 smt.arith.solver=6 small.smt2
sat
real  0m0.103s
user  0m0.030s
sys   0m0.011s
[561] % time z3release smt.arith.solver=2 small.smt2
sat
real  0m0.082s
user  0m0.016s
sys   0m0.000s
[562] % timeout -s 9 60 z3release smt.arith.solver=6 small.smt2
Killed
[563] %
[563] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun a () Real)
(assert (> 0 (div (to_int a) (to_int (* a (+ a 10000))))))
(check-sat)
[564] %

OS: Ubuntu 18.04 Commit: 6cc52e0

muchang commented 4 years ago

arith.solver=6 hangs on a simple QF_LIRA formula

[553] % time z3release smt.arith.solver=2 small.smt2
unsat
real  0m0.164s
user  0m0.012s
sys   0m0.003s
[554] % timeout -s 9 60 z3release smt.arith.solver=6 small.smt2
Killed
[555] % 
[555] % cat small.smt2
(set-logic QF_LIRA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Real)
(assert (= a (+ b c)))
(assert (< 0 c 1))
(check-sat)
[556] %

OS: Ubuntu 18.04 Commit: 1131fed

muchang commented 4 years ago

(1) arith.solver=2 gives the incorrect objective, i.e., (c ( (- 1.0) epsilon)), for the 2nd formula, while the correct one should be (c ( (- 1) oo); and (2) arith.solver=6 hangs on the 2nd formula.

[591] % time z3release smt.arith.solver=2 small.smt2
sat
(objectives
 (c (* (- 1) oo))
)
sat
(objectives
 (c (* (- 1.0) epsilon))
)
real  0m0.056s
user  0m0.012s
sys   0m0.004s
[592] % 
[592] % timeout -s 9 60 z3release smt.arith.solver=6 small.smt2
sat
(objectives
 (c (* (- 1) oo))
)
Killed
[593] % 
[593] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
; (assert (= (/ a b) 0))
(minimize c)
(check-sat)
(get-objectives)
(reset)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (= (/ a b) 0))
(minimize c)
(check-sat)
(get-objectives)
[594] %

OS: Ubuntu 18.04 Commit: 1131fed