mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 16:03:16 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-21 09:57:38 -08:00
parent 2932b63b1a
commit d0f0d5c3c6
1 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -328,15 +328,14 @@ namespace polysat {
return; 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)
continue; m_watch[v][j++] = idx;
m_watch[v][j++] = idx;
if (vars.size() <= 1) if (vars.size() <= 1)
continue; continue;
auto v0 = vars[0];
auto v1 = vars[1]; auto v1 = vars[1];
if (is_assigned(v1)) if (!is_assigned(v0) || is_assigned(v1))
continue; continue;
SASSERT(is_assigned(vars[0]) && vars.size() >= 2);
// detect unitary, add to viable, detect conflict? // detect unitary, add to viable, detect conflict?
m_viable.add_unitary(v1, idx); m_viable.add_unitary(v1, idx);
} }