diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-12 12:46:56 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-12 12:46:56 -0700 |
| commit | e3d75484ce558d862f7dfc80de9e88b56360b084 (patch) | |
| tree | ca66968c3c0455121efa00457438c0e6844293f3 /src/sat/bsat | |
| parent | 606341dca646b1f4282e19db20b62309e424477c (diff) | |
| download | abc-e3d75484ce558d862f7dfc80de9e88b56360b084.tar.gz abc-e3d75484ce558d862f7dfc80de9e88b56360b084.tar.bz2 abc-e3d75484ce558d862f7dfc80de9e88b56360b084.zip | |
Reversed to a buggy version of reduceDB in complete proof-logging, because it works with rollback and it is not used in &gla -pn -L 0.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 180659a4..74393a5b 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1619,10 +1619,10 @@ void sat_solver2_rollback( sat_solver2* s ) if ( s->pPrf1 ) { veci_resize(&s->claProofs, s->stats.learnts); -// Vec_SetShrink(&s->Proofs, s->hProofPivot); + Vec_SetShrink(s->pPrf1, s->hProofPivot); // some weird bug here, which shows only on 64-bits! // temporarily, perform more general proof reduction - Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot ); +// Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot ); } assert( s->pPrf2 == NULL ); // if ( s->pPrf2 ) |