Z3 reports incorrect model on NRA formula

[muchang]

Hi,
For this formula:

(declare-fun a () Real)
(declare-fun d () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun o () Real)
(declare-fun g () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun m () Real)

(assert (or
    (not (exists ((h Real))
            (=>
                (and (= (<= h (/ d k)) (>= (+ (* c h) (/ b m)) 0)) (>= o 0))
                (<= g (* (/ 1 2) (+ (* c (/ d k) (/ d k)) (* (* 2 (/ d k)) o) (* 2 g)))))))
    (not (exists ((i Real))
        (=> (> l 0) (= (>= e 0) (= (= (<= i e) (<= 0 f)) (= m 2))))))))
(assert (= a  (/ a c)))
(assert (= o m (/ b o)))
(check-sat)
(get-model)

z3 reports sat on this unsat formula and gives an incorrect model:

  (define-fun o () Real
    1.0)
  (define-fun b () Real
    1.0)
  (define-fun a () Real
    (- (/ 1.0 2.0)))
  (define-fun c () Real
    1.0)
  (define-fun m () Real
    1.0)
  (define-fun d () Real
    (/ 1.0 8.0))
  (define-fun k () Real
    0.0)
  (define-fun f () Real
    (- (/ 1.0 8.0)))
  (define-fun e () Real
    1.0)
  (define-fun l () Real
    1.0)

If I feed this model to the formula, z3 will report unsat.
z3-4.8.5 stable version will hang on this case.

OS:Ubuntu18.04
Revision: 9fa9aa0

[NikolajBjorner]

this may be fixed by now