mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

reset/set on successful superposition

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 11:06:45 +02:00
parent 640acd2ebc
commit d9eca1f40f
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -81,7 +81,11 @@ namespace polysat {
if (!c->contains_var(v)) {
core.keep(c);
core.remove_var(v);
// NOTE: more variables than 'v' might have been removed here (see polysat::test_p3), so remove_var(v) isn't enough.
// also, c alone (+ variables) is now enough to represent the conflict.
// core.remove_var(v);
core.reset();
core.set(c);
return l_true;
}
else