diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-25 19:39:32 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-25 19:39:32 -0400 |
| commit | ac74635e830b9b28e51eb6b3e2e04e98bc86bb72 (patch) | |
| tree | cf23a2f227fb49fa500fd3c9494a9e141c2b4d73 /src/prop/minisat | |
| parent | d8de492163b90974709a16918cb615515a536afc (diff) | |
Proposed fix for bug #513
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 8 |
1 files 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<Lit>& 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 |