qe-sat Assertion violation at ../src/qe/qe_sat_tactic.cpp Line: 634

Z3Prover / z3

The Z3 Theorem Prover

Other

10.17k stars 1.47k forks source link

qe-sat Assertion violation at ../src/qe/qe_sat_tactic.cpp Line: 634 #2966

Closed muchang closed 4 years ago

muchang commented 4 years ago

Hi, For this formula,

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ((c Real)) (= (>= 0.0 b) (= (<= c 0.0) (> a b)))))
(assert (forall ((d Real)) (< (/ (* (- a b) b) 0.0) a)))
(check-sat-using qe-sat)

z3 throws out an assertion violation:

Failed to verify: l_true == m_solvers[idx+1]->check()
ASSERTION VIOLATION
File: ../src/qe/qe_sat_tactic.cpp
Line: 634
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04 Revision: 524434c

NikolajBjorner commented 4 years ago

I am trying really hard to imagine a reasonable user having the urge to eliminate a quantified formula which contains abusive division by 0.

zhendongsu commented 4 years ago

Thanks for fixing this bug (and a lot of the other bugs that we filed), Nikolaj! The original unreduced test doesn't have such obvious divisions by 0.

NikolajBjorner commented 4 years ago

The case that seems to have been error prone is dealing correctly with semantics of underspecified operators, division, mod, remainder, power. They are bugs, but go under the radar as the use of these operators where the solver has to deal with underspecified behavior seems to have been pretty rare.