Non-deterministic assertion violation on NRA formula

[muchang]

Hi,
For this formula:

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

Z3 will throw out the assertion violation non-deterministically:

[700] % for i in $(seq 1 10); do echo "### $i-th run ###"; timeout -s 9 20 z3 small.smt2; echo; done;
### 1-th run ###
sat
### 2-th run ###
ASSERTION VIOLATION
File: ../src/math/polynomial/polynomial.cpp
Line: 800
m_monomials.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
### 3-th run ###
sat
### 4-th run ###
ASSERTION VIOLATION
File: ../src/math/polynomial/polynomial.cpp
Line: 800
m_monomials.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
### 5-th run ###
sat
### 6-th run ###
sat
### 7-th run ###
sat
### 8-th run ###
sat
### 9-th run ###
sat
### 10-th run ###
sat
[701] % cat small.smt2
(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 h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun aa () Real)
(assert
 (not
  (exists ((g Real))
   (=>
    (and
     (< (- (* (- (- h (- 24)) 1) (* (- (+ h (/ 8 k) (- k))) (* (+ 149 k) e)))) (- b d))
     (> e (+ 8 a) (* b d) 86)
     (> (/ 1 c i) (/ a j j))
     )
    (< e 0)))))
(assert (= (- k f) (- aa)))
(check-sat)
[702] %

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