diff options
| author | lianah <lianahady@gmail.com> | 2013-10-09 13:48:26 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-10-09 13:48:26 -0400 |
| commit | 08c8433e4ab849024930a8c4dbe8756e13d08099 (patch) | |
| tree | 2515d746c9b190e8770c5c690046410449900d7a /src/prop | |
| parent | 000f574406c29df4c60947169ef527ee5316beb7 (diff) | |
fixed uf proof bug: now storing deleted theory lemmas
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 45127a182..16fa3ba60 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -369,9 +369,8 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { - PROOF( ProofManager::getSatProof()->markDeleted(cr); ) - const Clause& c = ca[cr]; + PROOF( ProofManager::getSatProof()->markDeleted(cr); ) Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); |