Regression soundness bug from 4.8.8

[muchang]

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

[648] % z3-4.8.8 small.smt2
unsat
[649] % z3release small.smt2
sat
[650] % 
[650] % 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)
(assert
 (forall ((g Real))
 (and (< (- a d) 0.0 f)
  (>= 0 (mod 0 0))
  (>= (+ (* 0.5 (+ (* 2.0 (- e b) c) (- a d)))
    (/ (* (+ (* f (- b e)) (- c)) (+ (* f (- b e)) (- c)))
     (* 2.0 (- f))))
  0))))
(check-sat)
[651] %

OS: Ubuntu 18.04
Commit: a14c2a3

[NikolajBjorner]

release uses smt.arith.solver=2
disabling the nlsat code produces unknown

[NikolajBjorner]

@levnach - nlsat seems to produce the wrong answer. This is extremely likely duplicate reason related to other nlsat integration bugs, so easier to check the other cases before this.

[levnach]

Works correctly in f2d3160

./z3 ~/Dropbox/smts/4302.smt2 model_validate=true smt.arith.nl.nra=true
unsat
./z3 ~/Dropbox/smts/4302.smt2 model_validate=true smt.arith.nl.nra=false
unknown
cat ~/Dropbox/smts/4302.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)
(assert
(forall ((g Real))
(and (< (- a d) 0.0 f)
(>= 0 (mod 0 0))
(>= (+ (* 0.5 (+ (* 2.0 (- e b) c) (- a d)))
(/ (* (+ (* f (- b e)) (- c)) (+ (* f (- b e)) (- c)))
(* 2.0 (- f))))
0))))
(check-sat)
Compilation finished at Wed May 20 11:31:20