Incorrect result in NRA formula 4

[muchang]

Hi,
For this formula,

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun aa () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun o () Real)
(declare-fun ac () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun aj () Real)
(assert
 (not
  (exists ((o Real))
   (=>
    (or
     (and
      (or (and (<= g ad) (< (+ j (/ (* (- aa af) (- aa af)) (* c j))) 0) (<= 0 a)) (<= 0 l))
      (<= 0 (+ aa af)) (<= af l) (< 0 (/ 32 b (- e t))))
     (<= 0 l) (< 0 ac))
    (=> (<= 0 t) (not (=> (<= 0 o) (<= o ac))))))))
(assert
 (not
  (exists ((ak Real))
   (=>
    (and
     (or
      (and
       (or
        (and (= (or (<= 0 p) (<= p (* g k))) (<= 0 (+ (* d i a) a))) (<= 0 (- a f)) (< 0 (- b m)))
        (< (+ h (/ (* (- a f) (- a f)) (* 2 q))) n))
       (< n aj))
      (<= ae m))
     (< 0 (- m)))
    (<= 0 (+ (* (- d i) (- g k)) (- a f)))))))
(assert (= a (/ f r)))
(assert (= b (+ m ag)))
(assert (= c (+ n h )))
(assert (= g (+ k  s ag)))
(assert (= e (+ t ag) (+ o p ac r)))
(check-sat)
(get-model)

Z3 will incorrectly report sat, and give a model:

(define-fun r () Real
    0.0)
  (define-fun f () Real
    0.0)
  (define-fun a () Real
    1.0)
  (define-fun q () Real
    0.0)
  (define-fun b () Real
    (- 1.0))
  (define-fun af () Real
    (- (/ 1.0 8.0)))
  (define-fun aa () Real
    (- (/ 1.0 8.0)))
  (define-fun j () Real
    (- 1.0))
  (define-fun c () Real
    (- (/ 1.0 8.0)))
  (define-fun k () Real
    1.0)
  (define-fun g () Real
    (- (/ 1.0 8.0)))
  (define-fun i () Real
    (- 1.0))
  (define-fun d () Real
    2.0)
  (define-fun m () Real
    (- 2.0))
  (define-fun ac () Real
    (- 1.0))
  (define-fun p () Real
    (- (/ 1.0 16.0)))
  (define-fun o () Real
    (/ 49.0 16.0))
  (define-fun ag () Real
    1.0)
  (define-fun t () Real
    1.0)
  (define-fun e () Real
    2.0)
  (define-fun s () Real
    (- (/ 17.0 8.0)))
  (define-fun h () Real
    (- (/ 9.0 8.0)))
  (define-fun n () Real
    1.0)
  (define-fun aj () Real
    2.0)
  (define-fun ae () Real
    (/ 1.0 8.0))
  (define-fun l () Real
    1.0)
  (define-fun ad () Real
    1.0)

If I feed this model to the formula, z3 will report unsat.

OS: Ubuntu 18.04
Revision: a8049c7

[NikolajBjorner]

seems to be same root cause as #2650