luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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.

This commit is contained in:
Alan Mishchenko 2012-09-12 12:46:56 -07:00
parent 606341dca6
commit e3d75484ce
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/sat/bsat/satSolver2.c
View File

@ -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 )