Assertion violation on NRA formula

[muchang]

Hi,
For this formula:

(set-logic NRA)
(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)    
(declare-fun l () Real)   
(declare-fun m () Real)   
(declare-fun n () Real)   
(declare-fun o () Real)   
(declare-fun p () Real)   
(declare-fun q () Real)    
(declare-fun r () Real)   
(declare-fun s () Real)   
(declare-fun t () Real)   
(declare-fun u () Real)   
(declare-fun v () Real)   
(declare-fun w () Real)   
(declare-fun x () Real)   
(declare-fun y () Real)   
(declare-fun z () Real)   
(declare-fun aa () Real)   
(declare-fun ab () Real)   
(declare-fun ac () Real)   
(declare-fun ad () Real)   
(declare-fun ae () Real)   
(declare-fun af () Real)   
(declare-fun ag () Real)   
(declare-fun ah () Real)   
(declare-fun ai () Real)   
(declare-fun aj () Real)   
(declare-fun ak () Real)   
(declare-fun al () Real)   
(declare-fun am () Real)   
(declare-fun an () Real)   
(declare-fun ao () Real)   
(declare-fun ap () Real)  
(declare-fun aq () Real)   
(declare-fun ar () Real)   
(declare-fun at () Real)  
(declare-fun au () Real)   
(declare-fun av () Real)   
(declare-fun aw () Real)   
(assert
  (forall
    ((x Real))
    (or
      (<= 0.0 v)
      (and
        (=>
          (or (< 0.0 x) (>= x v))
          (and
            (or
              (and
                (<= 0.0 (/ 54 m al))
                (> (/ 60 m al) ac)
                (< 0.0 (+ c (* g v)))
              )
              (<= (- 4 c (/ 183 g v)) ac)
            )
            (>= x ae)
          )
        )
        (= (* 67 e (* 154 g v)) 2.0)
      )
      (= aw (+ aa al))
      (and
        (or
          (and
            (or
              (and (= ac q) (= (+ m al) 4))
              (= t 0.0)
            )
            (= t 2.0)
            (= u 2.0)
            (>
              (*
                y
                (-
                  (/ 232 n n)
                  (- (/ 19 ap (+ 64 f t)))
                )
              )
              w
            )
            (> 0.0 n ac)
            (<= ac (/ 245 b (/ 7 f t)))
          )
          (< 0.0 ac)
        )
        (< 0.0 ae)
      )
    )
  )
)
(assert
  (or
    (and
      (or
        (and
          (or
            (and
              (<
                0.0
                (+ (* (- ak) ai) (/ 85 b o))
              )
              (<= (+ ai (* b o)) (* j x))
              (>= 0.0 ai ar)
            )
            (> 0.0 ar)
          )
          (= (+ 89 e s) 0)
        )
        (<= o 53)
        (> (* b o) (/ 214 j x))
      )
      (= (+ aa af) 2.0)
      (<=
        (-
          (/ 63 k z)
          (- (- (/ 137 a n) (/ 21 a n) ak))
        )
        ah
      )
      (<= 0.0 ak)
      (> 0.0 (+ 249 a))
      (< (* a n) (* j x))
      (<= 0.0 (* d q))
      (< 0.0 (* j x))
    )
    (<= 0 (* j x))
  )
)
(assert (= a (+ n am)))
(assert (= b (+ 3 o aq)))
(assert (= c (* p ao)))
(assert (= d (* q aj aq r ai)))
(assert (= e (+ s ao)))
(assert (= f (/ 207 t aq)))
(assert (= at (+ u am)))
(assert (= g (+ 182 v ao)))
(assert (= h (/ 17 ab aj)))
(assert (= i (* w aj)))
(assert (= j (+ x an)))
(assert (= au (/ 119 y al)))
(assert (= k (+ z aw ac)))
(assert (= l (/ 9 ad ai)))
(assert (= av (/ ae ak)))
(assert (= aa (- af al)))
(assert (= m (/ 0 ag al)))
(check-sat)

Z3 will throw out the following assertion violation:

ASSERTION VIOLATION
File: ../src/util/mpbq.cpp
Line: 83
r == new_r
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 376d2c1