Soundness bug in NRA

[wintered]

Hi,

the following formula exposes a soundness bug in z3.

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

z3 gives sat, CVC4 gives unsat. Feeding the model to the formula gives an unknown result.

OS: Ubuntu 18.04
Revision: 1281964

[NikolajBjorner]

See #2650