Wrong model

[wintered]

Hi,

for this formula, we fed the model to formula and got unsat. Double-checking with CVC4 yields
unsat.

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

Model:

  (define-fun j () Real
    (- 1.0))
  (define-fun d () Real
    (- (/ 1.0 2.0)))
  (define-fun i () Real
    (/ 1.0 2.0))
  (define-fun c () Real
    (- 1.0))
  (define-fun m () Real
    0.0)
  (define-fun b () Real
    1.0)
  (define-fun g () Real
    1.0)
  (define-fun a () Real
    (- (/ 1.0 8.0)))
  (define-fun e () Real
    (- (/ 1.0 8.0)))
  (define-fun h () Real
    1.0)
  (define-fun f () Real
    0.0)
  (define-fun k () Real
    0.0)

OS: Ubuntu 18.05
Revision: 0c972b8