z3 incorrect sat on unsat NRA formula with exists

[muchang]

Hi,
For this formula:

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun aa () Real)
(declare-fun ab () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun j () Real)
(declare-fun g () Real)
(declare-fun i () Real)
(declare-fun h () Real)
(declare-fun k () Real)
(declare-fun ad () Real)
(declare-fun ag () Real)
(assert
 (not
  (exists ((ai Real))
   (=> (>= 0 c)
    (=> (<= 0 e)
     (or (> 0 ai) (> 0 (+ (* (+ b g) ai) aa)) (> (+ ai aa) (- i d))))))))
(assert
 (not
  (exists ((aj Real))
   (=
    (and
     (or (and (= (+ b e) (+ a f)) (<= f b)) (<= 0 ad))
     (= (- d i) 2)
     (< (+ ab (/ 0 (/ 2 k))) 0 k e a))
    (or
     (< (/ 1 c) (* 2 (/ (- 1) k)))
     (< (/ (* (+ (* k (- f b)) ad) (+ (* (/ (- 1) k) (- b f)) ad)) (* 2 k)) 0))))))
(assert (= b (+ f h)))
(assert (= c (+ j ag)(+ g h)))
(check-sat)

z3 gives incorrect sat answer and gives a model:

 (define-fun k () Real
    1.0)
  (define-fun ad () Real
    (- (/ 1.0 2.0)))
  (define-fun f () Real
    (/ 3.0 2.0))
  (define-fun b () Real
    2.0)
  (define-fun c () Real
    0.0)
  (define-fun h () Real
    (/ 1.0 2.0))
  (define-fun g () Real
    (- (/ 1.0 2.0)))
  (define-fun ag () Real
    (- (/ 1.0 4.0)))
  (define-fun j () Real
    (/ 1.0 4.0))
  (define-fun e () Real
    2.0)
  (define-fun a () Real
    (/ 5.0 2.0))
  (define-fun ab () Real
    (- 1.0))
  (define-fun i () Real
    (- 1.0))
  (define-fun d () Real
    1.0)
  (define-fun aa () Real
    (- (/ 29.0 4.0)))

If I feed this model to the formula, z3 reports unknown while cvc4 reports unsat.

OS: Ubuntu 18.04
Revision: 2f6a9ba

[NikolajBjorner]

Please file under #2650. Until this is resolved, no need for new NRA / QF_NRA issues but you can append additional examples to aid debugging. Two self-contained repros are under test/nlsat.cpp.