mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix blockers for pd-maxres

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-29 15:42:19 -07:00
parent e4ce6b6d74
commit dd01f6be46
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_solver.cpp
View file

@ -972,7 +972,14 @@ namespace sat {
} }
// backjump to last consistent assumption: // backjump to last consistent assumption:
unsigned j; unsigned j;
for (j = 0; j < i && value(lits[j]) == values[j]; ++j); m_weight = 0;
m_blocker.reset();
for (j = 0; j < i && value(lits[j]) == values[j]; ++j) {
if (values[j] == l_false) {
m_weight += weights[j];
m_blocker.push_back(lits[j]);
}
}
SASSERT(value(lits[j]) != values[j]); SASSERT(value(lits[j]) != values[j]);
SASSERT(j <= i); SASSERT(j <= i);
SASSERT(j == 0 || value(lits[j-1]) == values[j-1]); SASSERT(j == 0 || value(lits[j-1]) == values[j-1]);