z3 Incorrect result in NRA formula 2

Hi, For this formula,

(set-logic NRA)
(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)
(assert
  (not
    (exists
      ((t Real))
      (=>
        (and
          (or
            (and
              (=>
                (< 0 j)
                (and
                  (or
                    (<= 0 (+ (* n s) m))
                    (<= 0 p)
                  )
                  (> s 0)
                )
              )
              (<
                (*
                  o
                  (* (* n h) (/ o (- b h)))
                )
                0
              )
            )
            (< 0 n)
          )
          (< 0 p)
          (< 0 (- b h))
        )
        (<
          (/
            (* (+ (* n j) m) (+ (* n j) m))
            (* 2 o)
          )
          (* a e)
        )
      )
    )
  )
)
(assert
  (not
    (exists
      ((u Real))
      (=>
        (and
          (or (= (* c r) 0) (= l 0))
          (= e 2)
          (< h i (/ d r))
        )
        (=> (= 0 k) (not (<= u k 0 r)))
      )
    )
  )
)
(assert (= a (+ f o) (+ g o)))
(assert (= b (/ h q)))
(check-sat)
(get-model)

Z3 will incorrectly report sat, and give a model:

(define-fun h () Real
    (- 1.0))
  (define-fun b () Real
    0.0)
  (define-fun o () Real
    0.0)
  (define-fun q () Real
    0.0)
  (define-fun d () Real
    1.0)
  (define-fun m () Real
    1.0)
  (define-fun n () Real
    1.0)
  (define-fun j () Real
    1.0)
  (define-fun p () Real
    1.0)
  (define-fun s () Real
    (- 1.0))
  (define-fun g () Real
    (/ 1.0 2.0))
  (define-fun f () Real
    (/ 1.0 2.0))
  (define-fun a () Real
    (/ 1.0 2.0))
  (define-fun k () Real
    0.0)
  (define-fun l () Real
    (- 1.0))
  (define-fun r () Real
    1.0)
  (define-fun c () Real
    0.0)
  (define-fun i () Real
    0.0)
  (define-fun e () Real
    2.0)

If I feed this model to the formula, z3 will report unsat.

OS: Ubuntu 18.04 Revision: 9847675

Oct 22 '19 20:10 muchang

From #2700

(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 ag () Real)
(declare-fun ai () Real)
(assert
 (not
  (exists ((i Real))
   (= (and (= j (+ h (/ (* (- a ag) (- a ag)) 0)) 0) (<= ag 0))
    (= (<= 0 g) (= (> i 0) (<= f 0)))))))
(assert (not (exists ((aj Real)) (<= (+ ai (/ (* (+ 6 d) d) 0)) (/ d g c) (+ a e)))))
(assert (= a (+ e ag)))
(assert (= d (* j b)))
(check-sat)

Nov 14 '19 22:11 NikolajBjorner

From #2658

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun aa () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun o () Real)
(declare-fun ac () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun aj () Real)
(assert
 (not
  (exists ((o Real))
   (=>
    (or
     (and
      (or (and (<= g ad) (< (+ j (/ (* (- aa af) (- aa af)) (* c j))) 0) (<= 0 a)) (<= 0 l))
      (<= 0 (+ aa af)) (<= af l) (< 0 (/ 32 b (- e t))))
     (<= 0 l) (< 0 ac))
    (=> (<= 0 t) (not (=> (<= 0 o) (<= o ac))))))))
(assert
 (not
  (exists ((ak Real))
   (=>
    (and
     (or
      (and
       (or
        (and (= (or (<= 0 p) (<= p (* g k))) (<= 0 (+ (* d i a) a))) (<= 0 (- a f)) (< 0 (- b m)))
        (< (+ h (/ (* (- a f) (- a f)) (* 2 q))) n))
       (< n aj))
      (<= ae m))
     (< 0 (- m)))
    (<= 0 (+ (* (- d i) (- g k)) (- a f)))))))
(assert (= a (/ f r)))
(assert (= b (+ m ag)))
(assert (= c (+ n h )))
(assert (= g (+ k  s ag)))
(assert (= e (+ t ag) (+ o p ac r)))
(check-sat)
(get-model)

Z3 will incorrectly report sat, and give a model:

(define-fun r () Real
    0.0)
  (define-fun f () Real
    0.0)
  (define-fun a () Real
    1.0)
  (define-fun q () Real
    0.0)
  (define-fun b () Real
    (- 1.0))
  (define-fun af () Real
    (- (/ 1.0 8.0)))
  (define-fun aa () Real
    (- (/ 1.0 8.0)))
  (define-fun j () Real
    (- 1.0))
  (define-fun c () Real
    (- (/ 1.0 8.0)))
  (define-fun k () Real
    1.0)
  (define-fun g () Real
    (- (/ 1.0 8.0)))
  (define-fun i () Real
    (- 1.0))
  (define-fun d () Real
    2.0)
  (define-fun m () Real
    (- 2.0))
  (define-fun ac () Real
    (- 1.0))
  (define-fun p () Real
    (- (/ 1.0 16.0)))
  (define-fun o () Real
    (/ 49.0 16.0))
  (define-fun ag () Real
    1.0)
  (define-fun t () Real
    1.0)
  (define-fun e () Real
    2.0)
  (define-fun s () Real
    (- (/ 17.0 8.0)))
  (define-fun h () Real
    (- (/ 9.0 8.0)))
  (define-fun n () Real
    1.0)
  (define-fun aj () Real
    2.0)
  (define-fun ae () Real
    (/ 1.0 8.0))
  (define-fun l () Real
    1.0)
  (define-fun ad () Real
    1.0)

If I feed this model to the formula, z3 will report unsat.

OS: Ubuntu 18.04 Revision: a8049c7

Nov 14 '19 22:11 NikolajBjorner

From #2657 Hi, For this formula,

(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)
(assert (not (exists ((k Real)) (=> (< 0 j) (= (<= 0 f) (not (= (<= 0 f) (< (* d k f) e k j))))))))
(assert (not (= (< (/ (* (- a b) (- a b)) (* 2 i)) 0) (< 0 (* c h)))))
(assert (= a (/ b g)))
(check-sat)
(get-model)

Z3 will incorrectly report sat, and give a model:

 (define-fun g () Real
    (- 1.0))
  (define-fun b () Real
    (- (/ 1.0 4.0)))
  (define-fun a () Real
    (/ 1.0 4.0))
  (define-fun h () Real
    (/ 1.0 2.0))
  (define-fun c () Real
    (- 1.0))
  (define-fun i () Real
    (- 1.0))
  (define-fun j () Real
    1.0)
  (define-fun e () Real
    (- 1.0))
  (define-fun f () Real
    (- 1.0))
  (define-fun d () Real
    (- 2.0))

If I feed this model to the formula, z3 will report unsat.

OS: Ubuntu 18.04 Revision: a8049c7

Nov 14 '19 22:11 NikolajBjorner

(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 o () Real)
(assert
 (not
  (exists ((n Real))
   (=> (> d i) (= (<= 0 k) (not (=> (<= 0 n k) (and (= (+ (* b n) h) c) (= n (- d i))))))))))
(assert
 (not
  (exists ((m Real))
   (= (or (< (* l i i) 0 g) (< (+ j o) 0)) (or (< 0 a) (>= (+ (* 6 e) (/ i (* 2 l))) f))))))
(check-sat)

from #2729

Nov 22 '19 00:11 NikolajBjorner

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert
 (not
  (exists ((f Real))
   (=>
    (and (= c 0 (+ b (/ (/ e e) 0))) (< (+ a e) (+ d 1)) (>= a 0))
    (= (= f 0) (=> (> c (* a d)) (= b 0)))))))
(assert (= (+ d c e) 0))
(check-sat)

Jan 06 '20 14:01 wintered

Hi, For this case:

(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 p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(assert
 (forall ((o Real))
  (and
   (or
    (and
     (< (/ (* (- a q) (- a q)) (* 2 (- c h))) (- c (* d h)))
     (< q a)
     (<= (- a q) h)
     (< 0 r))
    (< 0 h))
   (<= 0 (* r o) i)
   (< (* (+ l (/ (* i i) 0)) (* (+ (/ g m) 1) q)) 0 i p)
   (= e 0)
   (< (+ n (/ (* r (- r)) (* 2 m))) 0 m)
   (< 0 (* b r) p)
   (< 0 q))))
(assert (= a (/ f q)))
(assert (= b (/ r k)))
(assert (= c (+ e j)))
(assert (= d (/ h j)))
(check-sat)
(get-mode)

z3 reports sat while this formula should be unsat. z3 gives this model as well:

(model 
  (define-fun j () Real
    3.0)
  (define-fun h () Real
    2.0)
  (define-fun r () Real
    1.0)
  (define-fun k () Real
    1.0)
  (define-fun f () Real
    2.0)
  (define-fun q () Real
    1.0)
  (define-fun m () Real
    1.0)
  (define-fun i () Real
    1.0)
  (define-fun g () Real
    (- 2.0))
  (define-fun a () Real
    2.0)
  (define-fun c () Real
    3.0)
  (define-fun d () Real
    (/ 2.0 3.0))
  (define-fun e () Real
    0.0)
  (define-fun b () Real
    1.0)
  (define-fun p () Real
    2.0)
  (define-fun n () Real
    (- 1.0))
  (define-fun l () Real
    1.0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    (ite (and (= x!0 2.0) (= x!1 3.0)) (/ 2.0 3.0)
    (ite (and (= x!0 1.0) (= x!1 1.0)) 1.0
    (ite (and (= x!0 2.0) (= x!1 1.0)) 2.0
    (ite (and (= x!0 (- 1.0)) (= x!1 2.0)) (- (/ 1.0 2.0))
    (ite (and (= x!0 1.0) (= x!1 0.0)) (/ 1.0 2.0)
    (ite (and (= x!0 (- 2.0)) (= x!1 1.0)) (- 2.0)
    (ite (and (= x!0 1.0) (= x!1 2.0)) (/ 1.0 2.0)
      0.0))))))))
)

If I feed this model to the formula, z3 will report unsat. It could be a new bug, since this formula contains quantifier forall rather than exists.

OS: Ubuntu 18.04 Revision: 9064e58

Jan 10 '20 05:01 muchang

The bugs are actually not because of the quantifiers. There are repros in the unit tests for nlsat_solver that exercise targeted scenarios. https://github.com/Z3Prover/z3/blob/9064e58665281c0e1db35d1f771bcec63945bbb4/src/test/nlsat.cpp#L751 It is of course more useful to have repros as close to the source of the bug as possible. So beyond just finding test cases, a more beneficial input is to include the bug localization analysis. There is a facility to validate clauses created by nlsat_solver. It isn't a perfect validator, as it passes some invalid learned clauses as if they are valid, but mostly ends up finding the bug in the post-analysis (in these cases, nlsat-solver is supposed to learn a tautology, but it isn't).

There isn't bandwidth to address the nlsat bugs for several months. Z3 is open source, you or others are invited to dig into this as bandwidth permits to go beyond the current state where bugs are filed without further analysis.

Jan 10 '20 06:01 NikolajBjorner

It seems all the bugs in this thread have been fixed. This thread can be closed.

Feb 02 '20 10:02 muchang

Hi, For this formula:

(set-option :rewriter.arith_ineq_lhs true)
(set-option :nlsat.shuffle_vars true)
(set-option :nlsat.randomize false)
(declare-fun e () Real) 
(declare-fun l () Real)
(declare-fun m () Real) 
(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun n () Real) 
(declare-fun f () Real) 
(declare-fun o () Real) 
(declare-fun p () Real) 
(declare-fun r () Real) 
(declare-fun g () Real)  
(declare-fun ep () Real) 
(declare-fun q () Real) 
(declare-fun h () Real) 
(assert (not (exists ((i Real)) 
(let ((?j m) (?k (+ i b))) (=> (and (> p (+ (+ q (/ (* r r) ?j) (+ (/ l l) r)))) 
(= g c f (+ (/ e ?j)) d 2 n) (= e a o))(=> (= h 0) (= (= ?k  0 ep) (distinct 2 2)))))))) 
(check-sat)

Z3 gives an incorrect answer:

$ z3/build/z3 small.smt2
sat
$ cat small.smt2 
(set-option :rewriter.arith_ineq_lhs true)
(set-option :nlsat.shuffle_vars true)
(set-option :nlsat.randomize false)
(declare-fun e () Real) 
(declare-fun l () Real)
(declare-fun m () Real) 
(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun n () Real) 
(declare-fun f () Real) 
(declare-fun o () Real) 
(declare-fun p () Real) 
(declare-fun r () Real) 
(declare-fun g () Real)  
(declare-fun ep () Real) 
(declare-fun q () Real) 
(declare-fun h () Real) 
(assert (not (exists ((i Real)) 
(let ((?j m) (?k (+ i b))) (=> (and (> p (+ (+ q (/ (* r r) ?j) (+ (/ l l) r)))) 
(= g c f (+ (/ e ?j)) d 2 n) (= e a o))(=> (= h 0) (= (= ?k  0 ep) (distinct 2 2)))))))) 
(check-sat)
$ z3/build/z3 small_without_opts.smt2
unsat
$ cat small_without_opts.smt2 
(declare-fun e () Real) 
(declare-fun l () Real)
(declare-fun m () Real) 
(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun n () Real) 
(declare-fun f () Real) 
(declare-fun o () Real) 
(declare-fun p () Real) 
(declare-fun r () Real) 
(declare-fun g () Real)  
(declare-fun ep () Real) 
(declare-fun q () Real) 
(declare-fun h () Real) 
(assert (not (exists ((i Real)) 
(let ((?j m) (?k (+ i b))) (=> (and (> p (+ (+ q (/ (* r r) ?j) (+ (/ l l) r)))) 
(= g c f (+ (/ e ?j)) d 2 n) (= e a o))(=> (= h 0) (= (= ?k  0 ep) (distinct 2 2)))))))) 
(check-sat)

OS: Ubuntu 18.04 Commit: 601b399

Mar 24 '20 17:03 NikolajBjorner

Another repro.

[677] % cvc4 -q small.smt2
unsat
[678] % z3 small.smt2
sat
[679] % 
[679] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun h () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun o () Real)
(declare-fun g () Real)
(declare-fun p () 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 ac () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(assert (forall ((ah Real)) (distinct (or (and (= g 2.0) (< (- (/ (* e e) 0)) i)) (<= e (/ h k))) (not (=> (<= ah l) (and (= n (* f ah) o) (>= (- ah o) k)))))))
(assert (exists ((ai Real)) (=> (or (<= (+ (/ (+ 1.0 ac) (- a e)) (- d p)) 0 ae 2.0) (<= 0.0 k)) (= b 2.0))))
(assert (= a (* m f af)))
(assert (distinct c (/ j ad)))
(check-sat)
[680] %

Apr 02 '20 12:04 wintered

Another instance:

[687] % cvc4 -q small.smt2
unsat
[688] % z3-4.8.7 small.smt2
unsat
[689] % z3-4.8.8 small.smt2
sat
[690] % z3release small.smt2
sat
[691] % 
[691] % 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 l () Real)
(declare-fun m () Real)
(assert (forall ((j Real)) (and (or (and (or (< (- (/ (* c c) 0)) f) (<= c (/ b m))))) (= (<= j 0) (and (<= 0.0 (+ (* d j) e)) (>= (- j e) b))))))
(assert (exists ((k Real)) (or (and (or (> (/ i (- a c)) 0) (> 0 l)) (> 0.0 m)) (>= 0.0 l))))
(assert (= a (* c h)))
(assert (= 0 (/ h e g)))
(check-sat)
[692] %

If I run it with the option tactic.default_tactic="(and-then simplify smt)" then z3 gives an "unsat". The "sat" is produced by nlqsat-tactic as I can tell from the verbose output.

May 22 '20 22:05 zhendongsu

Commit: https://github.com/Z3Prover/z3/commit/30e904bfa4ce7370b359a91ab9ab4c94bd6ee94a

Adding another refutation unsoundness instance:

[590] % z3release small.smt2
sat
[591] % z3release nlsat.inline_vars=true rewriter.eq2ineq=true small.smt2
unsat
[592] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (<= (- a) b))
(assert (> 1 (* c (/ 1 20))))
(assert (> 0 (div 0 0)))
(assert (<= 0 b))
(assert (= (- 1000 (* c c)) a (+ c (* c c))))
(check-sat)
[593] %

Apr 29 '21 08:04 zhendongsu

Commit: 51a4db8

[507] % z3release small.smt2
sat
[508] % z3release rewriter.cache_all=true nlsat.simplify_conflicts=false nlsat.shuffle_vars=true small.smt2
unsat
[509] % 
[509] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> b 0 c))
(assert (= (* b b) 2))
(assert (> (ite (= c 0) b (- (* a b b) b)) 0))
(check-sat)
[510] %

May 02 '21 19:05 zhendongsu

Commit: 51a4db8

[504] % z3release small.smt2
sat
[505] % z3release rewriter.eq2ineq=true small.smt2
unsat
[506] % 
[506] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (<= 0 a 1))
(assert (> b 0))
(assert (>= (* c (- (* a b) 1)) (* (/ 1 a))))
(assert (<= (* c (- (* a b) 1) (+ a b)) a))
(check-sat)
[507] %

May 02 '21 19:05 zhendongsu

Commit: https://github.com/Z3Prover/z3/commit/0c6722f48b2814e44ed98ea33b2a356579fd90f4

Solution unsoundness:

[593] % z3release small.smt2
unsat
[594] % z3release rewriter.flat=false model_validate=true small.smt2
sat
[595] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert
 (forall ((e Real))
  (and (and (and (=> (<= 0 e d) (>= (+ (- c (* e e)) (* e b)) 0)) (>= d 0)) (= c 0))
   (> (+ (- 1) b) (* e a)))))
(check-sat)
[596] %

May 04 '21 19:05 zhendongsu

Commit: 0c6722f

Another instance:

[588] % cvc4 -q small.smt2
unsat
[589] % z3release model_validate=true small.smt2
sat
[590] % 
[590] % 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)
(assert
 (forall ((j Real))
  (and (=> (<= j f) (xor (= (<= j f) (>= (+ (* (- c) j) d) 0)) (= d (/ a i d b e))))
   (>= d 0 (/ (* (/ (- (* 3 g)) 2) (/ (- (* 3 g)) 2)) (* 2 c)) h (/ (- (* 3 g)) 2))
   (< d (* c f)))))
(assert (= (+ c h) (/ a i d b e)))
(check-sat)
[591] %

May 04 '21 19:05 zhendongsu

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

Refutation unsoundness:

[701] % z3release small.smt2
sat
sat
[702] % z3release nlsat.simplify_conflicts=false nlsat.shuffle_vars=true rewriter.mul_to_power=true small.smt2
sat
unsat
[703] % 
[703] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (not (> (+ (* a b (+ b c)) c) 0)))
(assert (> c 2))
(assert (= c (- b 1)))
(push)
(check-sat)
(check-sat-using (then ctx-solver-simplify smt))
[704] %

May 30 '21 19:05 zhendongsu

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

Refutation soundness with nlsat.simplify_conflicts=false:

[551] % z3release small.smt2
sat
[552] % z3release nlsat.simplify_conflicts=false small.smt2
unsat
[553] % cat small.smt2
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> a 0))
(assert (<= a (+ c b (* c c)) a))
(assert (> c 0))
(assert (= (+ b (* (- 2 a) c)) 2))
(assert (= (+ (/ 2 b) (* a c)) 2))
(check-sat)
[554] %

levnach: does not reproduce in nls

Jun 01 '21 12:06 zhendongsu

Refutation unsoundness:

[547] % z3release small.smt2
sat
[548] % z3release rewriter.eq2ineq=true nlsat.shuffle_vars=true small.smt2
unsat
[549] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> a 0))
(assert (= (/ b a a) c (* a a a) (+ a (* a a))))
(check-sat)
[550] %

levnach: does not reproduce in nls

Jun 02 '21 10:06 zhendongsu

Moved from https://github.com/Z3Prover/z3/issues/5329

Commit: 7c86134 OS: Ubuntu 18.04 Note: affects all versions as early as z3-4.8.5

[512] % z3release small.smt2
sat
[513] % z3release nlsat.randomize=false small.smt2
unsat
[514] % cat small.smt2
(declare-fun a () Real)
(assert (forall ((b Real)) (exists ((c Real)) (and (= (+ a (* c (+ b c) (+ b c))) 0) (not (= a 0)) (> c 0)))))
(check-sat)
[515] %

Jun 04 '21 17:06 zhendongsu

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

Refutation unsoundness instance:

[591] % z3release small.smt2
unsat
sat
[592] % cat small.smt2
(set-option :rewriter.eq2ineq true)
(set-option :rewriter.flat false)
(set-option :nlsat.shuffle_vars true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(define-fun abs_real ((x Real)) Real (ite (>= x 0) x (- x)))
(assert (> (* c (- (/ 0 0))) (* a (* (/ 1 b (- 1 b)) (abs_real (* b b))))))
(assert (< b 0))
(check-sat)

(reset)

(set-option :rewriter.eq2ineq true)
(set-option :rewriter.flat false)
(set-option :nlsat.shuffle_vars true)
(define-fun a () Real (/ 1 8))
(define-fun b () Real (- 1.0))
(define-fun c () Real (/ (- 1) 8))
(define-fun abs_real ((x Real)) Real (ite (>= x 0) x (- x)))
(assert (> (* c (- (/ 0 0))) (* a (* (/ 1 b (- 1 b)) (abs_real (* b b))))))
(assert (< b 0))
(check-sat)
[593] %

levnach: does not reproduce in nls

Jun 13 '21 10:06 zhendongsu

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

Refutation unsoundness (regression from z3-4.8.8):

[508] % z3release small.smt2
sat
[509] % z3release nlsat.inline_vars=true rewriter.flat=false small.smt2
unsat
[510] % z3-4.8.11 nlsat.inline_vars=true rewriter.flat=false small.smt2
unsat
[511] % z3-4.8.10 nlsat.inline_vars=true rewriter.flat=false small.smt2
unsat
[512] % z3-4.8.8 nlsat.inline_vars=true rewriter.flat=false small.smt2
sat
[513] % cat small.smt2
(declare-fun a () Real)
(push)
(pop)
(assert (= (= (- (* a (- (* a a)))) (* a (* a a))) (= a 0)))
(check-sat)
[514] %

levnach: reproduces in nls

Jul 14 '21 17:07 zhendongsu

38250fc304ab66bf39613e669

(declare-const x Bool)
(declare-fun n () Real)
(declare-fun d () Real)
(declare-fun i () Real)
(declare-fun h () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(assert (and (forall ((j Real)) (and (< g n) (< 0.0 (+ d (* h f))) (= 0.0 (/ (* g g) f)) (or (> j f) (and (not x) (> 0.0 (+ d (* h j))))))) (= i (/ i d n))))
(check-sat)

z3 sat z3 tactic.default_tactic=smt sat.euf=true unsat cvc4 unsat

levnach: reproduces in nls

Jul 30 '21 08:07 rainoftime

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

Refutation unsoundness (regression from 4.8.10):

[514] % z3release small.smt2
sat
sat
sat
sat
sat
[515] % z3release rewriter.eq2ineq=true smt.arith.nl.tangents=false nlsat.shuffle_vars=true small.smt2
sat
sat
sat
sat
unsat
[516] % z3-4.8.11 rewriter.eq2ineq=true smt.arith.nl.tangents=false nlsat.shuffle_vars=true small.smt2
sat
sat
sat
sat
unsat
[517] % z3-4.8.10 rewriter.eq2ineq=true smt.arith.nl.tangents=false nlsat.shuffle_vars=true small.smt2
sat
sat
sat
sat
sat
[518] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(push)
(check-sat)
(check-sat)
(assert (= (* a (- 24 (* a a))) c))
(check-sat)
(assert (= (* a a) (- c 1)))
(assert (= (* b b) c))
(push)
(check-sat)
(pop)
(assert (> c 1))
(check-sat (< (* a a) 1))
[519] %

levnach: does not repro in nls

Aug 01 '21 11:08 zhendongsu

Soundness issue at commit ed3f8a52e6f010d14f9bfca39

(declare-fun n () Real)
(declare-fun d () Real)
(declare-fun i () Real)
(declare-fun h () Real)
(declare-fun c () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun l2 () Bool)
(declare-fun l3 () Bool)
(assert (let ((?x55 0.0)) (let (($x57 false)) (let (($x56 false)) (let (($x58 false)) (let (($x46 (let (($x44 false)) (let ((?x32 0.0)) (let (($x40 false)) (let (($x38 false)) (let (($x35 false)) (let (($x25 false)) (let (($x22 false)) (let (($x23 false)) (let (($x41 false)) false))))))))))) (let (($x47 false)) (and (forall ((j Real)) (not (let (($x44 false)) (let ((?x32 0.0)) (let (($x40 false)) (let (($x38 false)) (let (($x35 (= 0.0 (/ (* g g) c)))) (let (($x25 false)) (let (($x22 true)) (let (($x23 (> (+ d (* j (- c))) 0.0))) (let (($x41 (and $x35 (>= d 0.0) (> (- h) 0.0) (<= n (- g)) (or (not (and (<= 0.0 j) (<= j f))) $x23)))) (or (not $x41) (> (+ d (* f (- c))) 0.0))))))))))))) (= 0.0 (+ c h)) (= 1.0 (/ d i n))))))))))
(check-sat)

Aug 05 '21 03:08 rainoftime

Soundness issue in release 4.8.16

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert 
  (forall 
    ((e Real)) 
    (and
      (< c 0) 
      (= 0 (- e d (* a e e))) 
      (= b (- e d (* a e e)))
      (= b 
        (* 
          (+ 1 (- (* d 160)) (- 2 (/ (- (- 33 c)) (- 49) 2)))
          (+ 1 (- (* d 160)) (- 2 (/ (- (- 33 c)) (- 49) 2)))
        )
      )
    )
  )
)
(assert (= 0 0))
(check-sat)

Z3 incorrectly reports sat. Adding (set-logic NRA) or removing the second assert changes the output to unsat. Changing to (assert (= 1 1)) or (assert (= 2 2)) still triggers the bug, (assert (= 3 3)) and above seem not to.

A slight mutation of this with a boolean constant also fails:

(declare-const x Bool)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert 
  (forall 
    ((e Real)) 
    (and 
      (< c 0) 
      (= 0 (- e d (* a e e))) 
      (= b (- e d (* a e e))) 
      (= b 
        (* 
          (+ 1 (- (* d 80)) (- 1 (/ (- (- 16 c)) (- 24)))) 
          (+ 1 (- (* d 80)) (- 1 (/ (- (- 16 c)) (- 24))))
        )
      )
    )
  )
)
(assert x)
(check-sat)

Apr 29 '22 15:04 lweitzendorf

The above bug is confirmed in release 4.8.17 and was introduced in release 4.8.14.

It does not appear in releases 4.8.6 onwards until 4.8.13.

May 13 '22 09:05 nicdard

Soundness issue in releases 4.8.6 to 4.8.17.

(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(assert 
    (forall 
        ((e Real)) 
        (and 
            (= a 1) 
            (< c d)
            (or 
                (> e a)
                (= 1 (* b e))
            )
            (= 0 (/ (* (+ d 1) (+ a d)) a))         
        ) 
    ) 
)
(assert (= 0 (/ b c 0)))
(check-sat)

Z3 incorrectly reports sat. Adding (set-logic NRA) still triggers the bug.

OS: Ubuntu 20.04 levnach: reproduces in nls

May 14 '22 10:05 nicdard

Refutation unsoundness with rewriter.eq2ineq=true:

[609] % z3release small.smt2
sat
[610] % z3release rewriter.eq2ineq=true small.smt2
unsat
[611] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (> b 0))
(assert (= (* a a) 2))
(assert (= (* (- b a) (- b a)) 2))
(check-sat)

Jul 01 '22 17:07 zhendongsu

Transferred from https://github.com/Z3Prover/z3/issues/6145:

[546] % z3release small.smt2
sat
sat
[547] % z3debug small.smt2
sat
ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 143
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[548] % cat small.smt2
(set-option :nlsat.shuffle_vars true)
(set-option :smt.phase_selection 0)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (let ((f (+ a 1))) (and (<= b f) (distinct (* d d) (* c c)) (= 0 (/ 1 (* a a 1))) (> e 0))))
(check-sat)
(check-sat-using (then purify-arith ctx-solver-simplify smt))

Jul 11 '22 19:07 zhendongsu

z3 z3 copied to clipboard

Incorrect result in NRA formula 2

z3
z3 copied to clipboard