Assertion violations in algebraic_numbers.cpp, lines 389 and 390

[patrick96]

When running the following in z3 (compiled in debug mode):

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(assert (and
    (> d 0)
    (>= (* g g c (- 1)) 0)
    (= 0 (+ (* f e) (* h g)))
    (= b (+ h (- e) (* c i) (* f e (- b 1))))
    (or
        (= 0 (div a (* b b)))
        (distinct
            0
            (+ h (* d d c) (* d c (- d) (- i) (+ i g)))
        )
    )
))
(assert (>= c 0))
(assert (>= e 0))
(check-sat)

z3 produces two assertion violations:

$ z3-asan-8c95dff33 line389.smt2                                                                
ASSERTION VIOLATION
File: /home/patrick96/Projects/github.com/z3prover/z3/src/math/polynomial/algebraic_numbers.cpp
Line: 389
sl != sign_zero
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
c
ASSERTION VIOLATION
File: /home/patrick96/Projects/github.com/z3prover/z3/src/math/polynomial/algebraic_numbers.cpp
Line: 390
upm().eval_sign_at(c->m_p_sz, c->m_p, upper(c)) == -sl
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
c
sat

Expected behavior would be z3 just printing sat.

Z3 was compiled in debug mode with asan and ubsan:

cmake -DCMAKE_BUILD_TYPE=Debug -DZ3_INCLUDE_GIT_HASH=TRUE -DCMAKE_C_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer" -DCMAKE_CXX_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer" ..

I found this in 8c95dff and reproduced it on master (ea365de).

---

The input was reduced using ddSMT and manually cleaned up.

I also found #3684 which reported the same assertion violation. The issue was closed, but it seems because it set some solver options. Apologies if I misinterpreted this, feel free to close as a duplicate in that case.