mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 02:00:22 +00:00
Code Activity

bailout state: add premises of assignment

Browse source
This commit is contained in:
Jakob Rath 2022-07-25 13:49:21 +02:00
parent 1b370727b1
commit d65dc82ef0
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/conflict.cpp
View file

@ -499,9 +499,6 @@ namespace polysat {
s.inc_activity(v); s.inc_activity(v);
m_vars.remove(v); m_vars.remove(v);
if (is_bailout())
goto bailout;
if (j.is_propagation()) { if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v)) for (auto const& c : s.m_viable.get_constraints(v))
@ -512,6 +509,9 @@ namespace polysat {
} }
} }
if (is_bailout())
goto bailout;
LOG("try-explain v" << v); LOG("try-explain v" << v);
if (try_explain(v)) if (try_explain(v))
return true; return true;