From 8c162f0577bd825f3d1f81a1723fbd23f4c8d3a9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko 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(-) 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