Consolidated bugs in arithmetic logics #4532

wintered · 2020-06-18T15:20:50Z

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

The text was updated successfully, but these errors were encountered:

muchang · 2020-06-19T16:11:16Z

(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 6ced699

zhendongsu · 2020-06-20T15:26:35Z

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: 274323b
Does not repro in 6ced699

zhendongsu · 2020-06-20T15:56:27Z

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 · 2020-06-20T16:06:50Z

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 · 2020-06-20T17:30:05Z

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 · 2020-06-20T17:33:05Z

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 6ced699

zhendongsu · 2020-06-20T17:46:33Z

[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 · 2020-06-20T18:36:26Z

The last bug is not reproduced in 6524a70

zhendongsu · 2020-06-20T18:48:23Z

The last bug is not reproduced in 6524a70

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

zhendongsu · 2020-06-20T18:50:09Z

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: 6524a70
Does not repro in 6ced699

levnach · 2020-06-21T04:34:23Z

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 · 2020-06-21T17:29:45Z

An even simpler instance than the one in #4532 (comment) (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: 02f34ea
Does not repro in 6ced699

zhendongsu · 2020-06-21T17:39:29Z

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 · 2020-06-21T17:48:51Z

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 · 2020-06-22T15:19:34Z

A much simpler refutation soundness bug instance than the one in #4532 (comment):

[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: 02f34ea
This fixed in 6ced699

NikolajBjorner · 2020-06-22T19:20:27Z

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

zhendongsu · 2020-06-22T20:32:32Z

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 · 2020-06-22T21:02:36Z

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

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

zhendongsu · 2020-06-23T07:39:18Z

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 · 2020-06-23T10:14:19Z

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: 5d36578

zhendongsu · 2020-06-23T10:17:20Z

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 · 2020-06-23T12:40:58Z

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 · 2020-06-23T14:57:12Z

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 · 2020-06-29T21:51:56Z

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: 64f1a75

…bling rewriter.flat seems to be corner case exercised in #4532. Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

zhendongsu · 2020-07-18T15:43:37Z

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: a298091

zhendongsu · 2020-07-26T20:06:30Z

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: 4d586c2

NB: this is fixed
FIXED in 8857a67

zhendongsu · 2020-07-26T20:16:10Z

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 c7704ef

zhendongsu · 2020-07-31T17:08:36Z

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

muchang · 2020-08-20T18:17:19Z

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 · 2020-08-20T18:18:48Z

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 · 2020-08-21T02:37:59Z

(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 · 2020-08-21T02:44:54Z

(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 · 2020-08-21T02:57:16Z

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 · 2020-08-21T03:09:37Z

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 · 2020-09-18T04:03:42Z

(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 · 2020-09-18T09:48:11Z

(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 · 2020-09-21T11:00:11Z

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 · 2020-09-21T11:02:08Z

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 · 2020-09-23T02:09:57Z

Segmentation fault with declare-datatypes (might be the same as #4532 (comment))

[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 · 2020-10-01T16:58:31Z

(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 · 2020-10-05T02:26:47Z

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 · 2020-10-06T03:17:05Z

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 · 2020-10-06T03:20:03Z

(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

muchang · 2020-10-09T16:59:48Z

Invalid model on incremental QF_UFLIA formula

[590] % z3release model_validate=true small.smt2
sat
sat
sat
(error "line 8 column 10: an invalid model was generated")
(model 
 (define-fun a () Int
  0)
 (define-fun c ((x!0 Int)) Bool
  true)
 (define-fun b ((x!0 Int)) Bool
  false)
)
[591] % 
[591] % cat small.smt2
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(assert (= a 1))
(check-sat (b 1))
(check-sat)
(assert (c 2))
(check-sat)
(get-model)
[592] %

OS: Ubuntu 18.04
Commit: ae7d767

muchang · 2020-10-10T04:42:53Z

Another invalid model bug on incremental QF_UFLIA formula

[512] % z3release model_validate=true small.smt2
sat
sat
(error "line 47 column 10: an invalid model was generated")
(model 
 (define-fun a () Int
  0)
 (define-fun f ((x!0 Int)) Int
  0)
 (define-fun l ((x!0 Int)) Bool
  false)
 (define-fun i ((x!0 Int)) Bool
  false)
 (define-fun n ((x!0 Int)) Int
  0)
 (define-fun h ((x!0 Int)) Bool
  true)
 (define-fun g ((x!0 Int)) Int
  0)
 (define-fun c ((x!0 Int)) Bool
  true)
 (define-fun b ((x!0 Int)) Bool
  false)
 (define-fun d ((x!0 Int)) Bool
  false)
 (define-fun m ((x!0 Int)) Bool
  false)
 (define-fun k ((x!0 Int)) Bool
  false)
 (define-fun e ((x!0 Int)) Bool
  false)
 (define-fun j ((x!0 Int)) Bool
  false)
)
[513] % 
[513] % cat small.smt2
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(declare-fun d (Int) Bool)
(declare-fun e (Int) Bool)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-fun h (Int) Bool)
(declare-fun i (Int) Bool)
(declare-fun j (Int) Bool)
(declare-fun k (Int) Bool)
(declare-fun l (Int) Bool)
(declare-fun m (Int) Bool)
(declare-fun n (Int) Int)
(check-sat)
(assert (= (= (g 0) 1) (l 0)))
(assert (= (n 1) 0))
(assert
 (let ((n (g 1)))
 (let ((r (+ 2 n)) (s 0) (m (l 0)))
 (let ((ab (ite m 0 n)) (t (e 0)))
 (let ((u (ite t ab s)) (v 0) (w (j 0)))
 (let ((x (ite w v n)) (y (d 0)))
 (let ((z (ite y x u)) (ac (i 0)))
 (let ((ad (ite ac r n)) (ae (c 0)))
 (let ((af (ite ae ad z)) (ag (= a 0)))
 (let ((ah (ite ag 0 af)) (ai (g 2)))
  (= ai ah)))))))))))
(assert
 (let ((aj (n 0)) (ak 0) (al 0) (am (k 0)))
 (let ((an (ite am al aj)) (ao (m 0)))
 (let ((ap (ite ao an ak)) (aq 0) (ar (d 1)))
 (let ((ay (ite ar aq ap)) (bj 0) (at (b 0)))
 (let ((au (ite at bj ay)) (av (= a (- 1))))
 (let ((aw (ite av 7 au)) (ax (n 0)))
  (= ax aw))))))))
(assert (<= 1 (n 0)))
(assert
 (let ((az (f 0)))
 (let ((ba (<= 1 az)))
 (let ((bb (and ba)) (bc (g 0)))
 (let ((bd (= bc 0)))
 (let ((be (and bd bb)) (aj (n 2)))
 (let ((bf (= aj 0)))
 (let ((bg (and bf be)) (bh (h 0)))
  (= bh bg)))))))))
(check-sat)
(get-model)
[514] %

OS: Ubuntu 18.04
Commit: ae7d767

muchang · 2020-10-10T12:01:53Z

Invalid model bug on incremental QF_LIA formula

[643] % z3release model_validate=true small.smt2
sat
sat
sat
(error "line 7 column 10: an invalid model was generated")
(model 
 (define-fun b () Int
  1)
 (define-fun a () Int
  0)
)
[644] % 
[644] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(check-sat)
(assert (= a 1))
(check-sat)
(assert (distinct b 2))
(check-sat)
(get-model)
[645] %

OS: Ubuntu 18.04
Commit: ae7d767

muchang · 2020-10-22T05:43:05Z

z3 solution unsoundness (and the error from 4.8.8 is strange)

[532] % z3-4.8.7 small.smt2
unsat
[533] % z3-4.8.8 small.smt2
(error "line 2 column 23: unknown function/constant b")
sat
[534] % z3release small.smt2
sat
[535] % 
[535] % cat small.smt2
(define-fun b ((c Int)) Int 0)
(assert (= 1 (b (/ 1 1))))
(check-sat)
[536] %

Commit: 72d407a

muchang · 2020-11-05T09:29:05Z

Segmentation fault with smt.threads=2 on NIRA formula

[578] % z3release smt.threads=2 small.smt2
Segmentation fault
[579] % 
[579] % cat small.smt2
(assert (forall ((a Real) (b Real)) (xor (is_int a) (<= (/ 1 a (* (div 5 0) b)) (* (+ 2 a) (/ 0 b))))))
(check-sat)
[580] %

Commit: d0d06c2

muchang · 2020-11-13T16:41:45Z

Segmentation fault on the formula with seq

[531] % z3-4.8.8 small.smt2 
sat
[532] % z3release small.smt2 
Segmentation fault
[533] % 
[533] % cat small.smt2 
(declare-fun x () (Seq Int))
(declare-fun y () (Seq Int))
(declare-fun f ((Seq Int)) (Seq Bool))
(assert (distinct x y))
(assert (= (f x) (f y)))
(check-sat)
[534] %

Commit: cb4e519

#4532 (comment)

muchang · 2020-11-15T10:32:58Z

Segmentation fault on the formula with declare-datatypes

[542] % z3-4.8.8 small.smt2
sat
[543] % z3release small.smt2
Segmentation fault
[544] % 
[544] % cat small.smt2
(declare-datatypes ((a 0)) (((b (g Int)))))
(declare-sort c 0)
(declare-datatypes ((d 0)) (((o (r Bool) (e Int) (f c)))))
(declare-datatypes ((h 0)) (((i))))
(declare-datatypes ((j 0)) (((k (l h)))))
(declare-fun m (j) c)
(declare-sort p 0)
(declare-fun q (p d a) Bool)
(declare-fun v (d Int) p)
(declare-const w Int)
(declare-const aa Bool)
(declare-const n Int)
(declare-const x h)
(define-fun s () d (o aa w (m (k x))))
(assert (forall ((t d) (u a)) (distinct (q (v s n) t u) (= 0 (g u)))))
(check-sat)
[545] %

Commit: 49a0266

muchang · 2020-12-09T11:34:43Z

(purify-arith default) Invalid model for NIRA formula

[584] % z3release model_validate=true small.smt2
sat
(error "line 10 column 44: an invalid model was generated")
(
 (define-fun h () Real
  0.0)
 (define-fun d () Real
  (- 1.0))
 (define-fun c () Real
  2.0)
 (define-fun e () Real
  (- 1.0))
 (define-fun b () Real
  0.0)
 (define-fun f () Real
  0.0)
 (define-fun a () 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)
)
[585] % 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 h () Real)
(assert (forall ((g Real)) (xor (<= 0.0 (div (to_int g) (to_int h)) (mod 0 (to_int d)) e) (= c 2.0))))
(assert (= a (div (to_int b) (to_int f))))
(check-sat-using (then purify-arith default))
(get-model)
[586] %

Commit: 621e992

muchang · 2020-12-09T11:36:56Z

(purify-arith ufbv) Invalid model for NIRA formula

[571] % z3release model_validate=true small.smt2
sat
(error "line 12 column 41: an invalid model was generated")
( 
 (define-fun f () Real
  0.0)
 (define-fun b () Real
  (- 1.0))
 (define-fun a () Real
  0.0)
 (define-fun d () Real
  0.0)
 (define-fun h () Real
  (- 2.0))
 (define-fun c () Real
  0.0)
 (define-fun g () Real
  0.0)
 (define-fun e () Real
  (- 1.0))
 (define-fun div0 ((x!0 Int) (x!1 Int)) Int
  (ite (and (= x!0 1) (= x!1 (- 1))) (- 1)
  (ite (and (= x!0 4) (= x!1 0)) 1
   0)))
 (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
  (ite (and (= x!0 4) (= x!1 0)) (- 1)
   0))
)
[572] %
[572] % 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)
(assert (not (exists ((m Real)) (and (= 0 0) (<= 0.0 (mod (to_int f) (to_int m))) (= d 2.0)))))
(assert (> (div 4 (to_int a) (to_int b)) h))
(assert (= e (mod (to_int c) (to_int g))))
(check-sat-using (then purify-arith ufbv))
(get-model)
[573] %

Commit: 621e992

NikolajBjorner · 2021-04-12T01:06:58Z

bugs with qffd + arithmetic are 'wont-fix' (rocket)
bugs that touch nlsat are treated as duplicates (rocket)
many bugs are now seen as fixed (eyes)
several other without eyes/rocket are seen as duplicates (after triaging a sufficient number of instances). Refine a new consolidated if there is a miss.

NikolajBjorner added a commit that referenced this issue Jun 22, 2020

perf and div/mod axioms #4532

8758baf

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Jul 8, 2020

give up on addition subterms in monomial decomposition caused by disa…

e1a0a2e

…bling rewriter.flat seems to be corner case exercised in #4532. Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Jul 8, 2020

#4532 - arithmetic using SAT for interpreted atoms such as (< 0 0)

ec3066c

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

dylanjwolff mentioned this issue Aug 10, 2020

Soundness issue in NRA with rewriter.flat=false #4622

Closed

NikolajBjorner added a commit that referenced this issue Nov 13, 2020

#4532

c15001b

#4532 (comment)

NikolajBjorner added the Arithmetic label Dec 24, 2020

NikolajBjorner closed this as completed Apr 12, 2021

Consolidated bugs in arithmetic logics #4532

Consolidated bugs in arithmetic logics #4532

Comments

wintered commented Jun 18, 2020 • edited by levnach Loading

muchang commented Jun 19, 2020 • edited by levnach Loading

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

zhendongsu commented Jun 20, 2020 • edited by levnach Loading

zhendongsu commented Jun 20, 2020 • edited by levnach Loading

zhendongsu commented Jun 20, 2020 • edited by levnach Loading

zhendongsu commented Jun 20, 2020

zhendongsu commented Jun 20, 2020 • edited by levnach Loading

zhendongsu commented Jun 20, 2020 • edited Loading

levnach commented Jun 20, 2020

zhendongsu commented Jun 20, 2020

zhendongsu commented Jun 20, 2020 • edited by levnach Loading

levnach commented Jun 21, 2020 • edited Loading

zhendongsu commented Jun 21, 2020 • edited by levnach Loading

zhendongsu commented Jun 21, 2020

zhendongsu commented Jun 21, 2020

zhendongsu commented Jun 22, 2020 • edited by levnach Loading

NikolajBjorner commented Jun 22, 2020

zhendongsu commented Jun 22, 2020

NikolajBjorner commented Jun 22, 2020

zhendongsu commented Jun 23, 2020

zhendongsu commented Jun 23, 2020

zhendongsu commented Jun 23, 2020 • edited by NikolajBjorner Loading

zhendongsu commented Jun 23, 2020

zhendongsu commented Jun 23, 2020 • edited by levnach Loading

zhendongsu commented Jun 29, 2020

zhendongsu commented Jul 18, 2020

zhendongsu commented Jul 26, 2020 • edited Loading

zhendongsu commented Jul 26, 2020 • edited Loading

zhendongsu commented Jul 31, 2020

muchang commented Aug 20, 2020

muchang commented Aug 20, 2020

muchang commented Aug 21, 2020

muchang commented Aug 21, 2020 • edited Loading

muchang commented Aug 21, 2020 • edited Loading

muchang commented Aug 21, 2020

muchang commented Sep 18, 2020

muchang commented Sep 18, 2020

muchang commented Sep 21, 2020

muchang commented Sep 21, 2020

muchang commented Sep 23, 2020

muchang commented Oct 1, 2020

muchang commented Oct 5, 2020 • edited Loading

muchang commented Oct 6, 2020

muchang commented Oct 6, 2020 • edited Loading

muchang commented Oct 9, 2020

muchang commented Oct 10, 2020

muchang commented Oct 10, 2020

muchang commented Oct 22, 2020

muchang commented Nov 5, 2020 • edited Loading

muchang commented Nov 13, 2020

muchang commented Nov 15, 2020

muchang commented Dec 9, 2020

muchang commented Dec 9, 2020

NikolajBjorner commented Apr 12, 2021

wintered commented Jun 18, 2020 •

edited by levnach

Loading

muchang commented Jun 19, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 20, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 20, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 20, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 20, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 20, 2020 •

edited

Loading

zhendongsu commented Jun 20, 2020 •

edited by levnach

Loading

levnach commented Jun 21, 2020 •

edited

Loading

zhendongsu commented Jun 21, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 22, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 23, 2020 •

edited by NikolajBjorner

Loading

zhendongsu commented Jun 23, 2020 •

edited by levnach

Loading

zhendongsu commented Jul 26, 2020 •

edited

Loading

zhendongsu commented Jul 26, 2020 •

edited

Loading

muchang commented Aug 21, 2020 •

edited

Loading

muchang commented Aug 21, 2020 •

edited

Loading

muchang commented Oct 5, 2020 •

edited

Loading

muchang commented Oct 6, 2020 •

edited

Loading

muchang commented Nov 5, 2020 •

edited

Loading