Assertion violation at ../src/math/polynomial/polynomial.cpp Line: 801

[muchang]

Hi,
For this formula:

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

Z3 throws out an assertion violation:

[549] % z3 small.smt2
unsat
ASSERTION VIOLATION
File: ../src/math/polynomial/polynomial.cpp
Line: 801
m_monomials.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[550] % 
[550] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun n () Real)
(declare-fun k () Real)
(declare-fun d () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun l () Real)
(declare-fun g () Real)
(declare-fun m () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(assert (not (exists ((j Real)) (=> (and (=> (<= 0 j f) (<= j g)) (>=
 f 0) (= (/ c d) m) (> (/ a n) (+ m (/ (* l l) (* 2 (- (- b (-
 680.2932226634903)) k))) (* (+ (/ p e) 1) (+ (* (/ p 2) g g) (* g
 l))))) (>= l 0) (<= l (/ 0 0)) (< (/ a n) i) (> (- (- b (-
 680.2932226634903)) k) 0) (>= p 0)) (or (= h 7) (< o f ) (> (/ a n)
 (+ (* f l) (/ (* l l) (* 2 (- (- b (- 680.2932226634903))
 k))))))))))
(assert (= a (* n o)))
(assert (= o (/ a n)))
(assert (= b (+ e k (- 680.2932226634903))))
(assert (= d (/ c o)))
(assert (= o (/ c d)))
(check-sat)
[551] %

OS: Ubuntu 18.04
Commit: 38e0968

[NikolajBjorner]

We have seen this before. It wasn't addressed because it is due to cancellation and there is no real leak.
Since this bug was filed before in some guises and keeps reappearing I am changing behavior to not assert, but instead clean up gracefully. Otherwise, it isn't a behavior worth the overhead of changing.
Also, I wasn't able to reproduce it - it is timing dependent.