ASSERTION VIOLATION, File: ../src/math/polynomial/algebraic_numbers.cpp, Line: 2462

[zhendongsu]

Commit: e892904
OS: Ubuntu 22.04

[548] % z3debug small.smt2 
ASSERTION VIOLATION
File: ../src/math/polynomial/algebraic_numbers.cpp
Line: 2462
!nested_call
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[549] % cat small.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (> (* a c c) 0.0))
(assert (<= (* d c) (+ 1.0 (* b d) (* e e d e))))
(assert (< 0.0 c))
(assert (> d 1.0))
(assert (= 0.0 (+ d (* b c a))))
(assert (= 0.0 (+ 1.0 e a)))
(check-sat)

[NikolajBjorner]

some other bug had this assert too.

[zhendongsu]

Indeed: #5785

This one seems a lot simpler and manifests in the default mode.
All three tests from #5785 do not seem to reproduce anymore.