mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #2989

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-13 13:53:26 -10:00
parent 8ad939a10f
commit b96e203aea
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qe_arith_plugin.cpp
View file

@ -1022,7 +1022,10 @@ namespace qe {
//
// The first entry in values is the constant.
//
VERIFY(m_arith_solver.solve_integer_equation(values, index, is_aux));
if (!m_arith_solver.solve_integer_equation(values, index, is_aux)) {
// equation is unsat
return false;
}
SASSERT(1 <= index && index <= num_vars);
app_ref x(m_ctx.get_var(index-1), m);