mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

add hack for testing conflict resolution (but commented out)

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 14:49:56 +02:00
parent a8e68ebf86
commit c4e098b5d4
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/conflict_core.cpp
View file

@ -79,9 +79,11 @@ namespace polysat {
LOG("Conflict: " << c); LOG("Conflict: " << c);
SASSERT(empty()); SASSERT(empty());
insert(c); insert(c);
for (auto v : c->vars()) for (auto v : c->vars()) {
if (s().is_assigned(v)) if (s().is_assigned(v))
m_vars.insert(v); m_vars.insert(v);
// inc_pref(v); // hack to be able to test the rest of the conflict resolution loop, TODO: proper fix
}
SASSERT(!empty()); SASSERT(!empty());
} }