Skip to content

A
abc
Commit 8c162f05 by Alan Mishchenko
Options

Debugging a proof error.

parent 08bb2e70
Showing with 2 additions and 2 deletions
src/sat/bsat/satSolver2.c
...@@ -1571,8 +1571,8 @@ void sat_solver2_rollback( sat_solver2* s ) ...@@ -1571,8 +1571,8 @@ void sat_solver2_rollback( sat_solver2* s )
if ( s->fProofLogging ) if ( s->fProofLogging )
{ {
veci_resize(&s->claProofs, s->stats.learnts); veci_resize(&s->claProofs, s->stats.learnts);
Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here // Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here
// Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
} }
// initialize other vars // initialize other vars
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment