Assertion violation on NRA formula

[muchang]

Hi,
For this formula:

(declare-fun b () Real) 
(declare-fun KjafX_new () Real) 
(declare-fun c () Real) 
(declare-fun e () Real) 
(declare-fun a () Real) 
(declare-fun s () Real) 
(declare-fun l () Real) 
(declare-fun f () Real) 
(declare-fun d () Real) 
(declare-fun aa () Real) 
(declare-fun ac () Real) 
(declare-fun ts2209uscore0 () Real) 
(declare-fun g () Real) 
(declare-fun A () Real) 
(declare-fun m () Real) 
(declare-fun h () Real) 
(declare-fun V () Real) 
(declare-fun i () Real) 
(declare-fun o () Real) 
(declare-fun j () Real) 
(declare-fun n () Real) 
(assert
  (forall
    ((ts2209uscore0 Real))
    (or
      (<= 0 (/ 74 KjafX_new (/ a ts2209uscore0)))
      (>= 0 (/ e n))
      (and
        (>= (/ (/ s ts2209uscore0) aa) d)
        (>= (/ ts2209uscore0 0) 0)
      )
    )
  )
)
(assert
  (forall
    ((k Real))
    (or
      (and
        (or
          (and
            (or (>= 0 (/ b s)) (>= (/ 7 b s) i))
            (>= 0 j)
          )
          (>= (/ 5 c f) V)
          (= m 2)
          (>= 0 g)
          (<= h V)
        )
        (<= 0 (/ 0 l))
      )
      (>= 0 V)
    )
  )
)
(assert (= b (/ s o)))
(assert (= (/ ac A) a (/ ts2209uscore0 A)))
(check-sat)

z3 will throw out the assertion violation:

ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 1229
l != true_literal && l != false_literal
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

If I change the name of variable ts2209uscore0 to ad, z3 is able to report sat.
If I change the name of varibale KjafX_new to KjafX, z3 will report unknown.

OS: Ubuntu 18.04
Revision: fe7a7fe (./configure -d)