mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

missing continue fixes unsound sat result from #5573

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-29 14:26:09 -07:00
parent ff723f15ff
commit cbe7dd4a48
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_solver.cpp
View file

@ -490,6 +490,8 @@ namespace euf {
apply_solver(m_qsolver); apply_solver(m_qsolver);
if (num_nodes < m_egraph.num_nodes()) if (num_nodes < m_egraph.num_nodes())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
if (cont)
return sat::check_result::CR_CONTINUE;
TRACE("after_search", s().display(tout);); TRACE("after_search", s().display(tout););
if (give_up) if (give_up)
return sat::check_result::CR_GIVEUP; return sat::check_result::CR_GIVEUP;

4
src/sat/smt/q_ematch.cpp
View file

@ -605,7 +605,9 @@ namespace q {
} }
if (propagate(true)) if (propagate(true))
return true; return true;
return m_inst_queue.lazy_propagate(); if (m_inst_queue.lazy_propagate())
return true;
return false;
} }
void ematch::collect_statistics(statistics& st) const { void ematch::collect_statistics(statistics& st) const {