From 8c162f0577bd825f3d1f81a1723fbd23f4c8d3a9 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 13 Jul 2012 18:56:15 -0700
Subject: Debugging a proof error.
---
src/sat/bsat/satSolver2.c | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
(limited to 'src')
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 2cd825b7..bb81ccdd 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1571,8 +1571,8 @@ void sat_solver2_rollback( sat_solver2* s )
if ( s->fProofLogging )
{
veci_resize(&s->claProofs, s->stats.learnts);
- Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here
-// Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+// Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here
+ Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
}
// initialize other vars
--
cgit v1.2.3