From dd01f6be46a870c51d719343914d6dcd4d0564c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Aug 2015 15:42:19 -0700 Subject: [PATCH] fix blockers for pd-maxres Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e9562ddbb..7f54b0535 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -972,7 +972,14 @@ namespace sat { } // backjump to last consistent assumption: 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(j <= i); SASSERT(j == 0 || value(lits[j-1]) == values[j-1]);