mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

New constraints need to be eval'd

Browse source
This commit is contained in:
Jakob Rath 2022-09-27 17:56:26 +02:00
parent 602a9e3914
commit 0f993e3977
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/saturation.cpp
View file

@ -99,7 +99,7 @@ namespace polysat {
core.reset();
for (auto d : m_new_constraints)
core.insert(d);
core.insert_eval(d);
if (c.bvalue(s) != l_false) // conflict is due to the evaluation of c, so it depends on the variable values
core.insert_vars(c);
core.insert(~c);