search

Z3Prover / z3

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

Refutation unsoundness on NRA formula with => #4804

Closed muchang closed 7 months ago

muchang commented 3 years ago

It formulas should be sat, while Z3 reports unsat. Feeding model a = 0.0, b=0.0, c=1.0 to the formula makes Z3 reports sat. 

[584] % z3release small.smt2
unsat
sat
[585] % 
[585] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (not (exists ((d Real)) (=> (and (and (=> (=> (<= 0 d) (> d c)) (< (- b (* d d)) 0)) (= b 0)) (= a 0)) (= c 0)))))
(check-sat)
(reset)
(define-fun a () Real 0.0)
(define-fun b () Real 0.0)
(define-fun c () Real 1.0)
(assert (not (exists ((d Real)) (=> (and (and (=> (=> (<= 0 d) (> d c)) (< (- b (* d d)) 0)) (= b 0)) (= a 0)) (= c 0)))))
(check-sat)
[586] %

Commit: 40159a3 levnach: Reproduces in nls, transferred to https://github.com/Z3Prover/z3/issues/7174

muchang commented 3 years ago

From https://github.com/Z3Prover/z3/issues/4928

[536] % cvc4 -q small.smt2
sat
[537] % z3release smt.arith.solver=6 small.smt2
sat
[538] % z3release smt.arith.solver=2 small.smt2
unsat
[539] % 
[539] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(assert (= g (* g d) (+ (- 1) (* d h) a) (* a (- 1 g)) (+ f (* d g c) (- e) (* (* g b) 1)) 0))
(assert (>= d (+ f (* h c) (- e) (- (* d b)) (* g b)) (+ e d (- (+ d h)) (- (* h h c))) 0))
(assert (distinct (+ (mod d b) g) (* d c) 0))
(assert (>= d 0))
(assert (>= g 0))
(assert (>= h f))
(check-sat)
[540] %

Commit: 4db41c0 levnach: does not reproduce in nls With smt.random_seed=1 in smt.arith.solver=6:

[609] % z3release small.smt2
sat
[610] % z3release smt.random_seed=1 small.smt2
unsat
[611] % cat small.smt2
(declare-fun w^01 () Int)
(declare-fun e^01 () Int)
(declare-fun y^01 () Int)
(declare-fun Nl23__const_8^01 () Int)
(declare-fun Nl23d^01 () Int)
(declare-fun o^01 () Int)
(declare-fun Nl23sqr11^01 () Int)
(declare-fun w^02 () Int)
(declare-fun e^02 () Int)
(declare-fun y^02 () Int)
(declare-fun Nl23__const_8^02 () Int)
(declare-fun Nl23d^02 () Int)
(declare-fun o^02 () Int)
(declare-fun Nl23sqr11^02 () Int)
(declare-fun f () Int)
(declare-fun p () Int)
(declare-fun lam0n3 () Int)
(declare-fun v () Int)
(declare-fun lam0n6 () Int)
(declare-fun z () Int)
(declare-fun x () Int)
(declare-fun q () Int)
(declare-fun g () Int)
(declare-fun a () Int)
(declare-fun r () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun s () Int)
(declare-fun lam2n7 () Int)
(declare-fun j () Int)
(declare-fun ^ () Int)
(declare-fun ^0 () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun k () Int)
(declare-fun lam5n7 () Int)
(declare-fun t () Int)
(declare-fun l () Int)
(declare-fun d () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun aa () Int)
(declare-fun u () Int)
(declare-fun lam6n8 () Int)
(assert (<= o^01 1Nl23sqr11^01))
(assert (<= y^02 1))
(assert (<= 0 Nl23__const_8^02 1))
(assert (<= o^02 1))
(assert (or (and (>= lam0n3 0) (>= v 0) (> (+ p lam0n3) 0) (= (+ (+ 1
   v) (* w^02 z)) 0 (+ p e^02) 0 (+ (- (- 1) lam0n3 v) (* y^02 z)))
   (distinct v 0) (= Nl23d^02 0 (+ p (* o^01 lam0n6) (* o^02 z)) 0 (*
   Nl23sqr11^01 lam0n6))) (and (> x 0) (= (- w^01) a 0 (* Nl23sqr11^02
   r) (- Nl23sqr11^01)))))
(assert (or (and (= w^02 0 (mod e^01 lam0n6) 0 (+ (* y^02 z)) 0
   Nl23d^01 0 (div 0 g))) (and (>= i 0) (> (* q lam2n7) 0) (= h 2 (*
   Nl23d^01 s)) (= (- Nl23sqr11^02) 0))))
(assert (and (<= (+ q (* 2 ^0) (* e^02 ^0 2)) 0) (or (and (>= b c k t
   0) (> t 0) (= e^02 y^02 (+ (* ^ lam5n7) Nl23__const_8^02) (* ^
   lam5n7) 0 l d m)) (and (>= n aa u 0) (>= lam6n8 (* q lam6n8) 0) (=
   (+ (* w^02 lam6n8) 1) 0 (+ aa (* e^02 lam6n8)) (+ (* y^01 u))) (=
   (+ (* Nl23__const_8^01 u) (* Nl23__const_8^02 lam6n8)) (+ (*
   Nl23d^02 lam6n8)) (+ (* o^01 u) (* o^02 lam6n8)) (* ^ lam6n8) 0))
   (and (= j (div 0 0) 0) (>= f z 0 (+ v (* Nl23__const_8^02)) 0
   z)))))
(check-sat)
[612] %

Commit: 4db41c0 levnach: does not reproduce in nls

muchang commented 3 years ago

Refutational soundness bug on QF_NIA formula z3_ref_unsound_large.smt2.zip

[510] % z3-4.8.8 z3_ref_unsound_large.smt2 
sat
[511] % z3release smt.arith.solver=2 z3_ref_unsound_large.smt2 
sat
[512] % z3release smt.arith.solver=6 z3_ref_unsound_large.smt2 
unsat
[513] %

Commit: 8abb644 levnach: Does not reproduce in nls

muchang commented 3 years ago

(rewriter.flat=false) z3 refutation unsoundness in nlsat

[677] % z3release small.smt2
sat
[678] % z3release rewriter.flat=false small.smt2
unsat
[679] % 
[679] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert
 (let ((d b))
 (and (<= (mod 0 (to_int (* a (+ (/ 1 3000000000) (mod (to_int a) 0))))) 0)
  (> a 0)
  (> c b)
  (= (* c c) (/ 1 (* b (- b)))))))
(check-sat)
[680] %

Commit: 8abb644 levnach: does not reproduce in nls

muchang commented 3 years ago

(ctx-solver-simplify) Refutation unsoundness 

[620] % z3release small.smt2
unsat
sat
[621] % 
[621] % cat small.smt2
(declare-fun a () Real)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun xe () Bool)
(declare-fun xh () Real)
(declare-fun xm () Real)
(declare-fun e () Bool)
(declare-fun xj () Real)
(declare-fun xl () Real)
(declare-fun xr () Real)
(declare-fun f () Real)
(declare-fun xo () Real)
(declare-fun h () Bool)
(declare-fun xp () Real)
(declare-fun xq () Real)
(declare-fun g () Real)
(declare-fun yd () Real)
(declare-fun ab () Bool)
(declare-fun ye () Real)
(declare-fun xs () Real)
(declare-fun yf () Real)
(declare-fun yg () Real)
(declare-fun yh () Real)
(declare-fun yi () Real)
(assert
(let ((zs (and (and false))))
(let ((zt (and (or true))))
(let ((zu (and zt)))
(let ((zv (and zu)))
(let ((zw (and zv)))
(let ((zx (or zw)))
(let ((aa (* (- 1.0) f)))
(let ((x (and (and (or zx)))))
(let ((bs (and (and (and (= ab d))))))
(let ((bv (= xj yf)))
(let ((bb (= 0 0.0)))
(let ((cc (and true)))
(let ((ds (and (not h))))
(let ((d (and (= h ab))))
(let ((b (and (and (and (= c h))))))
(let ((fh (and (= xe c))))
(let ((gz (and (= e c))))
 (and (= yd 10.0) (= yi 0.0) (or (<= (+ f (* yi yi)) 0.0)
 (not (distinct yd xl))) (and (= (+ yi xo) 0.0) (<= 0.0
 xl)(and (and (= xl xq) (or (and (= xo xs)))))) (= (+ xq (+ (*
 xs yh) (* aa (* yh yh)))) 0.0) (not (= yh 0.0)) (or (and
 (= xh 1.0))) (or c (<= (* (- 1.0) (* xm xm)) 0.0) (= a xr)) (=
 (+ xm xr) 0.0 (+ xh xp))(= xr g) (= xp yg)(= (+ g (* aa (*
 ye ye))) 0.0) (= (+ yg (* aa ye)) 0.0))))))))))))))))))))
(check-sat-using ctx-solver-simplify)
(check-sat)
[622] %

Commit: 2d1684b levnach: does not reproduce in nls

muchang commented 3 years ago

Hi, here is a refutation soundness bug that is only on the debug build:

[619] % z3release small.smt2
sat
[620] % cvc4 -q small.smt2
sat
[621] % z3debug small.smt2
unsat
[622] % 
[622] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun o () Int)
(declare-fun p () Int)
(assert
 (or
 (and (>= m 0)
  (> (* i d) 0)
  (= (mod 1 c) 0)
  (>= c 0)
  (>= d 0)
  (= (+ (- m) a (* e d)) (+ c (* f d)) 0))))
(assert (<= (+ (* a o) j) 0 (+ i (* e o) (* f j)) 0))
(assert
 (or
 (and (>= g 0 p l (* h k) 0)
  (= (+ g (* a k) (+ e l))
  (+ (- 1) k (* f l))
  (+ g (* b k) 2 (* n k))
  0))))
(check-sat)
[623] %

Commit: 20870c4 levnach: does not reproduce in nls

muchang commented 3 years ago

(smt.arith.solver=6) refutation unsoundness on QF_NIA formula

[606] % z3release smt.arith.solver=2 small.smt2
sat
[607] % cvc4 -q small.smt2
sat
[608] % z3release smt.arith.solver=6 small.smt2
unsat
[609] % 
[609] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun aa () Int)
(assert (= (* c d) 0))
(assert (>= (- (* d b) e) (div (- 1) f) 0))
(assert (>= (+ (* a m) (- a i j (* a j d k))) 0 (mod g (* g k))))
(assert (>= j 1 (+ (* a j) (div (- 1) (* a aa f)) (- (* a m d))) 0))
(assert (>= (+ l (* i e) (- (* i b)) (- (* m k d b))) 0))
(assert (not (= l i)))
(assert (<= 0 a 1))
(assert (>= b 0))
(assert (>= d k 0))
(assert (>= m h i 0))
(assert (< l 0))
(check-sat)
[610] %

Commit: 615cafe

levnach: works in branch nls.

muchang commented 3 years ago

Refutation unsoundness on QF_NRA formula

[184] % z3release incorrect.smt2
unsat
[185] % cat incorrect.smt2 
(declare-fun scr1_skoX () Real)
(declare-fun scr1_skoS () Real)
(declare-fun scr1_skoC () Real)
(declare-fun scr2_skoX () Real)
(declare-fun scr2_skoS () Real)
(declare-fun scr2_skoC () Real)
(declare-fun scr1_skoS_scr2_skoS_fused () Real)
(declare-fun scr1_skoC_scr2_skoX_fused () Real)
(declare-fun scr1_skoX_scr2_skoC_fused () Real)
(assert (and (and (and (<= (* (- scr1_skoX_scr2_skoC_fused scr2_skoC) (+ (+ (* scr1_skoC (/ (- 14336) 55)) (* scr1_skoS (/ 395136 1375))) (* scr1_skoX (+ (+ (* scr1_skoC (/ 25088 6875)) (* scr1_skoS (/ (- 691488) 171875))) (* scr1_skoX (+ (+ (* scr1_skoC (/ (- 87808) 2578125)) (* scr1_skoS (/ 806736 21484375))) (* scr1_skoX (+ (+ (* scr1_skoC (/ 67228 322265625)) (* scr1_skoS (/ (- 2470629) 10742187500))) (* scr1_skoX (+ (+ (* (- (- scr1_skoC_scr2_skoX_fused scr2_skoX) 597.47046) (/ (- 33614) 40283203125)) (* scr1_skoS (/ 2470629 2685546875000))) (* scr1_skoX (+ (* scr1_skoC (/ 117649 60424804687500)) (* scr1_skoS (/ (- 5764801) 2685546875000000)))))))))))))) (+ (* scr1_skoC (/ (- 102400) 11)) (* scr1_skoS (/ 112896 11)))) (and (<= (- scr1_skoX_scr2_skoC_fused scr2_skoC) 0) (and (not (<= (* scr1_skoX (+ (/ 8352 625) (* (- scr1_skoX_scr2_skoC_fused scr2_skoC) (+ (/ 15138 390625) (* scr1_skoX (+ (/ 73167 976562500) (* scr1_skoX (+ (/ 14852901 156250000000000) (* scr1_skoX (+ (/ 61533447 781250000000000000) (* scr1_skoX (/ 594823321 15625000000000000000000)))))))))))) (- 2304))) (and (= (* scr1_skoS scr1_skoS) (+ 1 (* scr1_skoC (* scr1_skoC (- 1))))) (and (<= scr1_skoX 75) (<= 0 scr1_skoX))))))) (and (and (<= (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (+ (* scr2_skoC (/ (- 14336) 55)) (* scr2_skoS (/ 395136 1375))) (* scr2_skoX (+ (+ (* scr2_skoC (/ 25088 6875)) (* scr2_skoS (/ (- 691488) 171875))) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (+ (* scr2_skoC (/ (- 87808) 2578125)) (* scr2_skoS (/ 806736 21484375))) (* scr2_skoX (+ (+ (* scr2_skoC (/ 67228 322265625)) (* scr2_skoS (/ (- 2470629) 10742187500))) (* scr2_skoX (+ (+ (* scr2_skoC (/ (- 33614) 40283203125)) (* (- (- scr1_skoS_scr2_skoS_fused (- 385.2477)) scr1_skoS) (/ 2470629 2685546875000))) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (* scr2_skoC (/ 117649 60424804687500)) (* scr2_skoS (/ (- 5764801) 2685546875000000)))))))))))))) (+ (* scr2_skoC (/ (- 102400) 11)) (* scr2_skoS (/ 112896 11)))) (and (<= (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) 0) (and (not (<= (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 8352 625) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 15138 390625) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 73167 976562500) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 14852901 156250000000000) (* scr2_skoX (+ (/ 61533447 781250000000000000) (* scr2_skoX (/ 594823321 15625000000000000000000)))))))))))) (- 2304))) (and (= (* scr2_skoS scr2_skoS) (+ 1 (* (- scr1_skoX_scr2_skoC_fused scr1_skoX) (* (- scr1_skoX_scr2_skoC_fused scr1_skoX) (- 1))))) (and (<= (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) 75) (<= 0 (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046))))))))))
(check-sat)
(exit)
[186] % z3release withmodel.smt2 
sat
[187] % cat withmodel.smt2 
(define-fun scr1_skoX () Real 0.0)
(define-fun scr1_skoS () Real (/ 1.0 8.0))
(define-fun scr1_skoC () Real (root-obj (+ (* 64 (^ x 2)) (- 63)) 1))
(define-fun scr2_skoX () Real 0.0)
(define-fun scr2_skoS () Real (/ 1.0 8.0))
(define-fun scr2_skoC () Real (root-obj (+ (* 64 (^ x 2)) (- 63)) 1))
(declare-fun scr1_skoS_scr2_skoS_fused () Real)
(declare-fun scr1_skoC_scr2_skoX_fused () Real)
(declare-fun scr1_skoX_scr2_skoC_fused () Real)
(assert (and (and (and (<= (* (- scr1_skoX_scr2_skoC_fused scr2_skoC) (+ (+ (* scr1_skoC (/ (- 14336) 55)) (* scr1_skoS (/ 395136 1375))) (* scr1_skoX (+ (+ (* scr1_skoC (/ 25088 6875)) (* scr1_skoS (/ (- 691488) 171875))) (* scr1_skoX (+ (+ (* scr1_skoC (/ (- 87808) 2578125)) (* scr1_skoS (/ 806736 21484375))) (* scr1_skoX (+ (+ (* scr1_skoC (/ 67228 322265625)) (* scr1_skoS (/ (- 2470629) 10742187500))) (* scr1_skoX (+ (+ (* (- (- scr1_skoC_scr2_skoX_fused scr2_skoX) 597.47046) (/ (- 33614) 40283203125)) (* scr1_skoS (/ 2470629 2685546875000))) (* scr1_skoX (+ (* scr1_skoC (/ 117649 60424804687500)) (* scr1_skoS (/ (- 5764801) 2685546875000000)))))))))))))) (+ (* scr1_skoC (/ (- 102400) 11)) (* scr1_skoS (/ 112896 11)))) (and (<= (- scr1_skoX_scr2_skoC_fused scr2_skoC) 0) (and (not (<= (* scr1_skoX (+ (/ 8352 625) (* (- scr1_skoX_scr2_skoC_fused scr2_skoC) (+ (/ 15138 390625) (* scr1_skoX (+ (/ 73167 976562500) (* scr1_skoX (+ (/ 14852901 156250000000000) (* scr1_skoX (+ (/ 61533447 781250000000000000) (* scr1_skoX (/ 594823321 15625000000000000000000)))))))))))) (- 2304))) (and (= (* scr1_skoS scr1_skoS) (+ 1 (* scr1_skoC (* scr1_skoC (- 1))))) (and (<= scr1_skoX 75) (<= 0 scr1_skoX))))))) (and (and (<= (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (+ (* scr2_skoC (/ (- 14336) 55)) (* scr2_skoS (/ 395136 1375))) (* scr2_skoX (+ (+ (* scr2_skoC (/ 25088 6875)) (* scr2_skoS (/ (- 691488) 171875))) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (+ (* scr2_skoC (/ (- 87808) 2578125)) (* scr2_skoS (/ 806736 21484375))) (* scr2_skoX (+ (+ (* scr2_skoC (/ 67228 322265625)) (* scr2_skoS (/ (- 2470629) 10742187500))) (* scr2_skoX (+ (+ (* scr2_skoC (/ (- 33614) 40283203125)) (* (- (- scr1_skoS_scr2_skoS_fused (- 385.2477)) scr1_skoS) (/ 2470629 2685546875000))) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (* scr2_skoC (/ 117649 60424804687500)) (* scr2_skoS (/ (- 5764801) 2685546875000000)))))))))))))) (+ (* scr2_skoC (/ (- 102400) 11)) (* scr2_skoS (/ 112896 11)))) (and (<= (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) 0) (and (not (<= (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 8352 625) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 15138 390625) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 73167 976562500) (* (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) (+ (/ 14852901 156250000000000) (* scr2_skoX (+ (/ 61533447 781250000000000000) (* scr2_skoX (/ 594823321 15625000000000000000000)))))))))))) (- 2304))) (and (= (* scr2_skoS scr2_skoS) (+ 1 (* (- scr1_skoX_scr2_skoC_fused scr1_skoX) (* (- scr1_skoX_scr2_skoC_fused scr1_skoX) (- 1))))) (and (<= (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046) 75) (<= 0 (- (- scr1_skoC_scr2_skoX_fused scr1_skoC) 597.47046))))))))))
(check-sat)
(exit)
[188] %

Z3 gives unsat on this formula, while if I feed a part of the model, Z3 gives sat.

Commit: f59ff7c levnach: does not reproduce in nls