Refutation soundness bug in QF_NIA

[muchang]

[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

[muchang]

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

[NikolajBjorner]

These are really duplicates of bug in nlsat

[muchang]

Thanks, Nikolaj, shall we close it due to the duplication?

[NikolajBjorner]

can be moved to one of those bugs labeled nlsat

[muchang]

Moved to #4804