z3 wrong model & assertion violation

[wintered]

Hi,
for this formula z3 gives a wrong model

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

Model:

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

The model is wrong since the first and evaluates to false as -1/4 >= 0 does not hold for
(>= (+ (* e l) (/ c j)) 0). In turn, the outermost (=> evaluates to true which is negated by a not, i.e. the first assertion simplifies to false. Feeding the model to the formula results in an assertion violation

ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 631
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Revision: 000e485 (assertions enabled)
OS: Ubuntu 18.04