mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

bugfix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-08 20:44:30 -08:00
parent cc4ed602e5
commit f34e55e86e
1 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/smt/polysat/core.cpp
View file

@ -358,7 +358,7 @@ namespace polysat {
void core::propagate_assignment(pvar v, rational const& value, dependency dep) { void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
TRACE("bv", tout << "propagate assignment v" << v << " := " << value << "\n"); TRACE("bv", tout << "propagate assignment v" << v << " := " << value << "\n");
SASSERT(!is_assigned(v));
m_values[v] = value; m_values[v] = value;
m_justification[v] = dep; m_justification[v] = dep;
m_assignment.push(v , value); m_assignment.push(v , value);
@ -390,12 +390,18 @@ namespace polysat {
// will not update m_watch[v] (other than copy constructor for m_watch) // will not update m_watch[v] (other than copy constructor for m_watch)
// because v has been assigned a value. // because v has been assigned a value.
propagate_eval({ idx }); propagate_eval({ idx });
if (s.inconsistent())
return;
SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1]))); SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
if (!swapped) if (!swapped)
m_watch[v][j++] = idx; m_watch[v][j++] = idx;
if (s.inconsistent()) {
++k;
for (; k < sz; ++k)
m_watch[v][j++] = m_watch[v][k];
m_watch[v].shrink(j);
return;
}
if (vars.size() <= 1) if (vars.size() <= 1)
continue; continue;
auto v0 = vars[0]; auto v0 = vars[0];