mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix check against looping

Browse source
This commit is contained in:
Jakob Rath 2022-06-29 14:27:11 +02:00
parent 0fb8c72f50
commit 69a28a7740
1 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1,4 +1,4 @@
/*++
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
@ -72,7 +72,6 @@ namespace polysat {
LOG("critical " << m_rule << " " << crit1);
LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s) << " " << core.contains(~c));
// ensure new core is a conflict
if (!c.is_currently_false(s) && c.bvalue(s) != l_false)
return false;
@ -81,7 +80,20 @@ namespace polysat {
return false;
// avoid loops
if (core.contains(~c))
// NOTE:
// it is not enough to only check whether ~c is already in the core.
// One example had c: 0 != 0, so c was ignored when inserting it to the core.
// (But the side conditions in m_new_constraints were useful.)
bool inserting = false;
if (!c.is_always_false() && !core.contains(~c))
inserting = true;
else
for (auto d : m_new_constraints)
if (!d.is_always_true() && !core.contains(d)) {
inserting = true;
break;
}
if (!inserting)
return false;
core.reset();