Incorrect result in NRA formula 2 #2650

muchang · 2019-10-22T20:19:48Z

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

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

…le tree whenever possible Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

NikolajBjorner · 2019-11-14T22:14:04Z

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)

NikolajBjorner · 2019-11-14T22:15:33Z

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

NikolajBjorner · 2019-11-14T22:17:32Z

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

NikolajBjorner · 2019-11-22T00:46:44Z

(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

wintered · 2020-01-06T14:30:50Z

(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)

muchang · 2020-01-10T05:45:20Z

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

NikolajBjorner · 2020-01-10T06:01:05Z

The bugs are actually not because of the quantifiers.
There are repros in the unit tests for nlsat_solver that exercise targeted scenarios.

z3/src/test/nlsat.cpp

Line 751 in 9064e58

project_fa(s, ex, x, 2, lits.c_ptr());

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.

muchang · 2020-02-02T10:01:08Z

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

NikolajBjorner · 2020-03-24T17:29:44Z

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

wintered · 2020-04-02T12:58:13Z

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] %

zhendongsu · 2020-05-22T22:46:42Z

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.

zhendongsu · 2021-06-01T12:35:25Z

Commit: ba56bfa
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

zhendongsu · 2021-06-02T10:25:26Z

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

zhendongsu · 2021-06-04T17:29:16Z

Moved from #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] %

zhendongsu · 2021-06-13T10:53:59Z

Commit: 082ec0f
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

zhendongsu · 2021-07-14T17:53:18Z

Commit: 79c2617
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

rainoftime · 2021-07-30T08:20:00Z

38250fc

(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

zhendongsu · 2021-08-01T11:11:24Z

Commit: e148eea
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

rainoftime · 2021-08-05T03:47:17Z

Soundness issue at
commit ed3f8a5

(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)

lweitzendorf · 2022-04-29T15:27:32Z

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)

nicdard · 2022-05-13T09:57:06Z

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.

nicdard · 2022-05-14T10:35:24Z

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

zhendongsu · 2022-07-01T17:57:43Z

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)

zhendongsu · 2022-07-11T19:32:41Z

Transferred from #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))

zhendongsu · 2022-07-15T07:05:09Z

[623] % z3release small.smt2 
unknown
[624] % z3debug small.smt2 
ASSERTION VIOLATION
File: ../src/math/grobner/pdd_solver.cpp
Line: 369
m_solved.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[625] % cat small.smt2
(set-option :smt.arith.nl.horner false)
(set-option :smt.random_seed 7)
(set-option :smt.phase_selection 1)
(declare-fun sko () Real)
(declare-fun koB () Real)
(declare-fun s () Real)
(assert (>= 0 sko))
(assert (distinct 1.0 0.0))
(assert (= 0 (* sko (+ sko (* (+ sko sko (- 1)) (/ (+ s s) (/ koB (- koB 1))))))))
(assert (<= 2 koB))
(assert (= koB s))
(check-sat-using (then purify-arith ctx-solver-simplify))

wintered · 2022-07-20T14:14:17Z

81cb575

$z3release bug.smt2                                                             
sat                                                                             
$cvc5 -q bug.smt2                                                               
unsat                                                                           
$cat bug.smt2                                                                   
(declare-fun n () Real)                                                         
(declare-fun f () Real)                                                         
(declare-fun o () Real)                                                         
(declare-fun g () Real)                                                         
(declare-fun h () Real)                                                         
(assert (forall ((j Real)) (and (< n g) (= o (* (- g) (- g))) (or (> 0 j) (= j h) 
             (and (<= j o) (= 0 (+ 1.0 (* j f))))))))
(assert (= o (/ 0.0 n)))                                                        
(check-sat)%

zhendongsu · 2022-11-20T08:55:44Z

[556] % z3release small.smt2
sat
[557] % z3debug small.smt2
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
[558] % cat small.smt2
(set-option :nlsat.simplify_conflicts false)
(set-option :nlsat.shuffle_vars true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (not (> (+ (* (+ (* 31 a) (* (- 7) c)) a) c (* (- 8) b)) (- 725) a)))
(assert (= (+ (- c) (* 6 a)) (- 1)))
(assert (or (> c 0) (< b 0)))
(check-sat-using (then ctx-solver-simplify smt))

levnach: does not reproduce in nls

zhendongsu · 2023-08-20T19:52:09Z

[550] % z3release model_validate=true small.smt2
sat
sat
(
  (define-fun b () Real
    (/ 11.0 80.0))
  (define-fun a () Real
    (- 83.0))
  (define-fun c () Real
    (- (/ 331.0 4.0)))
)
[551] % z3release nlsat.simplify_conflicts=false nlsat.reorder=false smt.arith.nl.order=false model_validate=true small.smt2
sat
unsat
(error "line 10 column 10: model is not available")
[552] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (>= (* (- a b) a) 0))
(check-sat)
(assert (= (+ (* 2 a) (* 1200 b)) (- 1)))
(assert (< (* (+ 10 c) b) (- 10)))
(assert (< a c 0))
(check-sat)
(get-model)

levnach: does not reproduce in nls

NikolajBjorner · 2023-11-14T15:42:06Z

[518] % z3release model_validate=true small.smt2
unsat
sat
[519] % cat small.smt2
(set-option :rewriter.eq2ineq true)
(set-option :nlsat.shuffle_vars true)
(set-option :nlsat.factor false)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (<= (* a (+ 24.0 (* (ite (> 5.0 d) (* a (+ 24.0 (* a (+ (- 120.0) (* 240.0 a))))) (* a a)) (+ (- 120.0) (* 240.0 a))))) 2.0))
(assert (= (* b b) (+ 1.0 d)))
(assert (= (* a a) (- d 1.0)))
(assert (= (* c c) d))
(assert (> d 1.0))
(assert (> c 0.0))
(assert (> (/ 5.0 (+ (- 120.0) (* 240.0 a)) (+ (- 120.0) (* 240.0 a)) a) d))
(check-sat)

(reset)

(set-option :rewriter.eq2ineq true)
(set-option :nlsat.shuffle_vars true)
(set-option :nlsat.factor false)
(define-fun a () Real (/ 47.0 96.0))
(define-fun d () Real (/ 11425.0 9216.0))
(declare-fun b () Real)
(declare-fun c () Real)
(assert (<= (* a (+ 24.0 (* (ite (> 5.0 d) (* a (+ 24.0 (* a (+ (- 120.0) (* 240.0 a))))) (* a a)) (+ (- 120.0) (* 240.0 a))))) 2.0))
(assert (= (* b b) (+ 1.0 d)))
(assert (= (* a a) (- d 1.0)))
(assert (= (* c c) d))
(assert (> d 1.0))
(assert (> c 0.0))
(assert (> (/ 5.0 (+ (- 120.0) (* 240.0 a)) (+ (- 120.0) (* 240.0 a)) a) d))
(check-sat)

levnach: does not reproduce in nls

janisozaur pushed a commit to janisozaur/z3 that referenced this issue Oct 23, 2019

fix Z3Prover#2650, use datatype constructor producing smallest possib…

02e71c7

…le tree whenever possible Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Oct 24, 2019

unit test for #2650

60dde9f

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

NikolajBjorner added the bug label Oct 24, 2019

NikolajBjorner mentioned this issue Oct 25, 2019

Incorrect result in NRA formula 4 #2658

Closed

NikolajBjorner mentioned this issue Nov 14, 2019

Soundness bug in NRA #2700

Closed

NikolajBjorner mentioned this issue Dec 8, 2019

z3 incorrect sat on unsat NRA formula with exists #2783

Closed

muchang closed this as completed Feb 2, 2020

NikolajBjorner reopened this Mar 23, 2020

This was referenced Mar 23, 2020

Soundness bug on NRA formula (master + debug) without options #3484

Closed

:rewriter.arith_ineq_lhs :nlsat.shuffle_vars :nlsat.randomize Soundness bug on NRA formula #3501

Closed

NikolajBjorner mentioned this issue Apr 11, 2020

Soundness issue with nlsat.shuffle_vars=true #3914

Closed

wintered mentioned this issue Apr 25, 2020

Soundness bug in NRA #4096

Closed

NikolajBjorner mentioned this issue Apr 27, 2020

Soundness bug default mode unsat (incorrect), ewriter.eq2ineq=true sat (correct) #4129

Closed

NikolajBjorner mentioned this issue Jun 11, 2020

Soundness issues for QF_NRA formulas #4491

Closed

zhendongsu mentioned this issue Jun 21, 2020

Consolidated bugs in arithmetic logics #4532

Closed

zhendongsu mentioned this issue Oct 10, 2020

Issues in arithmetic and string logics #4525

Closed

NikolajBjorner mentioned this issue Nov 14, 2020

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

Closed

NikolajBjorner added the nlsat Non-linear polynomial solver label Jan 24, 2021

NikolajBjorner mentioned this issue Apr 8, 2021

Refutation soundness issue on a QF_NRA formula #5161

Closed

NikolajBjorner mentioned this issue Jun 4, 2021

(nlsat.randomize=false) refutation soundness issue on NRA formula #5329

Closed

NikolajBjorner mentioned this issue Aug 24, 2021

Issues with tactics #5502

Closed

This was referenced Mar 7, 2022

(rewriter.eq2ineq,nlsat.shuffle_vars) Refutational soundness issue on QF_NRA #5883

Closed

Care for root index being undefine while calling Z3_algebraic_get_i() #5888

Merged

nicdard mentioned this issue May 4, 2022

Bug tracking nicdard/fusion-function-generator#37

Merged

KJongUk mentioned this issue Jul 4, 2022

Refutation soundness bug in QF_NRA #6130

Closed

zhendongsu mentioned this issue Jul 11, 2022

ASSERTION VIOLATION: File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp, Line: 143 #6145

Closed

zhendongsu mentioned this issue Jul 17, 2022

(rewriter.sort_sums) solution soundness issue #6167

Closed

zhendongsu mentioned this issue Dec 8, 2022

refutation unsoundness on a QF_NIA instance #6484

Closed

zhendongsu mentioned this issue Mar 26, 2023

Solution unsoundness on arithmetic #6647

Closed

zhendongsu mentioned this issue Nov 2, 2023

refutation unsoundness issue on QF_NRA formula #6981

Closed

merlinsun mentioned this issue Nov 10, 2023

Invalid model issue on QF_NRA #6988

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Incorrect result in NRA formula 2 #2650

Incorrect result in NRA formula 2 #2650

muchang commented Oct 22, 2019

NikolajBjorner commented Nov 14, 2019

NikolajBjorner commented Nov 14, 2019

NikolajBjorner commented Nov 14, 2019

NikolajBjorner commented Nov 22, 2019

wintered commented Jan 6, 2020

muchang commented Jan 10, 2020

NikolajBjorner commented Jan 10, 2020

muchang commented Feb 2, 2020

NikolajBjorner commented Mar 24, 2020

wintered commented Apr 2, 2020

zhendongsu commented May 22, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 1, 2021 •

edited by levnach

Loading

zhendongsu commented Jun 2, 2021 •

edited by levnach

Loading

zhendongsu commented Jun 4, 2021

zhendongsu commented Jun 13, 2021 •

edited by levnach

Loading

zhendongsu commented Jul 14, 2021 •

edited by levnach

Loading

rainoftime commented Jul 30, 2021 •

edited by levnach

Loading

zhendongsu commented Aug 1, 2021 •

edited by levnach

Loading

rainoftime commented Aug 5, 2021 •

edited

Loading

lweitzendorf commented Apr 29, 2022 •

edited

Loading

nicdard commented May 13, 2022

nicdard commented May 14, 2022 •

edited by levnach

Loading

zhendongsu commented Jul 1, 2022

zhendongsu commented Jul 11, 2022

zhendongsu commented Jul 15, 2022

wintered commented Jul 20, 2022 •

edited

Loading

zhendongsu commented Nov 20, 2022 •

edited by levnach

Loading

zhendongsu commented Aug 20, 2023 •

edited by levnach

Loading

NikolajBjorner commented Nov 14, 2023 •

edited by levnach

Loading

Incorrect result in NRA formula 2 #2650

Incorrect result in NRA formula 2 #2650

Comments

muchang commented Oct 22, 2019

NikolajBjorner commented Nov 14, 2019

NikolajBjorner commented Nov 14, 2019

NikolajBjorner commented Nov 14, 2019

NikolajBjorner commented Nov 22, 2019

wintered commented Jan 6, 2020

muchang commented Jan 10, 2020

NikolajBjorner commented Jan 10, 2020

muchang commented Feb 2, 2020

NikolajBjorner commented Mar 24, 2020

wintered commented Apr 2, 2020

zhendongsu commented May 22, 2020 • edited by levnach Loading

zhendongsu commented Jun 1, 2021 • edited by levnach Loading

zhendongsu commented Jun 2, 2021 • edited by levnach Loading

zhendongsu commented Jun 4, 2021

zhendongsu commented Jun 13, 2021 • edited by levnach Loading

zhendongsu commented Jul 14, 2021 • edited by levnach Loading

rainoftime commented Jul 30, 2021 • edited by levnach Loading

zhendongsu commented Aug 1, 2021 • edited by levnach Loading

rainoftime commented Aug 5, 2021 • edited Loading

lweitzendorf commented Apr 29, 2022 • edited Loading

nicdard commented May 13, 2022

nicdard commented May 14, 2022 • edited by levnach Loading

zhendongsu commented Jul 1, 2022

zhendongsu commented Jul 11, 2022

zhendongsu commented Jul 15, 2022

wintered commented Jul 20, 2022 • edited Loading

zhendongsu commented Nov 20, 2022 • edited by levnach Loading

zhendongsu commented Aug 20, 2023 • edited by levnach Loading

NikolajBjorner commented Nov 14, 2023 • edited by levnach Loading

zhendongsu commented May 22, 2020 •

edited by levnach

Loading

zhendongsu commented Jun 1, 2021 •

edited by levnach

Loading

zhendongsu commented Jun 2, 2021 •

edited by levnach

Loading

zhendongsu commented Jun 13, 2021 •

edited by levnach

Loading

zhendongsu commented Jul 14, 2021 •

edited by levnach

Loading

rainoftime commented Jul 30, 2021 •

edited by levnach

Loading

zhendongsu commented Aug 1, 2021 •

edited by levnach

Loading

rainoftime commented Aug 5, 2021 •

edited

Loading

lweitzendorf commented Apr 29, 2022 •

edited

Loading

nicdard commented May 14, 2022 •

edited by levnach

Loading

wintered commented Jul 20, 2022 •

edited

Loading

zhendongsu commented Nov 20, 2022 •

edited by levnach

Loading

zhendongsu commented Aug 20, 2023 •

edited by levnach

Loading

NikolajBjorner commented Nov 14, 2023 •

edited by levnach

Loading