Soundness bug on incremantal QF_NIRA formula

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[779] % cvc4 --incremental small.smt2
sat
sat
sat
sat
[780] % z3release small.smt2
sat
sat
sat
unsat
[781] % 
[781] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (or (< (+ a b) 0) (< (* 6 c) (- 5))))
(push)
(assert (or (>= a 2) (> a 0)))
(check-sat)
(pop)
(assert (> (+ (* 48 b) (* 26 a c)) (- 3)))
(assert (<= (- b c) 1))
(check-sat)
(push)
(assert (not (<= (+ a c) 3)))
(check-sat)
(pop)
(assert (not (< (* (- 9) a) 37)))
(assert (or (not (= c 3 )) (< (mod 9 (to_int c)) 5 (div (- 4) (to_int b)))))
(assert (= (+ c (* (- 7) b)) 9))
(check-sat)
[782] %

OS: Ubuntu 18.04
Commit: 9c97252

[muchang]

Here is another case:

[689] % cvc4 --incremental small.smt2
sat
[690] % z3release small.smt2
unsat
[691] % 
[691] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (not (= a 9)))
(push)
(pop)
(assert (>= (+ (* a b) a) 8))
(assert (or (>= a 0) (> (/ 7 a) 0) (distinct (div 4 (to_int b)) 0)))
(check-sat)
[692] %

[NikolajBjorner]

same regression as exposed by the other recent unsoundndess bugs