mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 13:47:01 +00:00
Code Activity

viable conflict also depends on vars

Browse source
This commit is contained in:
Jakob Rath 2022-11-22 13:40:29 +01:00
parent 6e72a97727
commit 33ea8d6e57
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/viable.cpp
View file

@ -701,6 +701,7 @@ namespace polysat {
lemma.insert_eval(~sc); lemma.insert_eval(~sc);
lemma.insert(~e->src); lemma.insert(~e->src);
core.insert(e->src); core.insert(e->src);
core.insert_vars(e->src);
e = n; e = n;
} }
while (e != first); while (e != first);