From ac74635e830b9b28e51eb6b3e2e04e98bc86bb72 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 25 Jun 2013 19:39:32 -0400 Subject: [PATCH] Proposed fix for bug #513 --- src/prop/minisat/core/Solver.cc | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 4cce83fef..cacde258d 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -135,6 +135,8 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), true); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), true); ) } @@ -298,9 +300,9 @@ bool Solver::addClause_(vec& ps, bool removable) if (ps[i] == p) { continue; } - // If a literals is false at 0 level (both sat and user level) we also ignore it - if (value(ps[i]) == l_False && !PROOF_ON() ) { - if (level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + // If a literal is false at 0 level (both sat and user level) we also ignore it + if (value(ps[i]) == l_False) { + if (!PROOF_ON() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { continue; } else { // If we decide to keep it, we count it into the false literals -- 2.30.2