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

fixed a tricky bug: property should not be assumed true in the last frame

This commit is contained in:
Yen-Sheng Ho 2017-02-19 19:57:44 -08:00
parent 1a66a5823a
commit 25ecc3d429
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/proof/pdr/pdrIncr.c
View File

@ -99,7 +99,6 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p )
assert( RetValue == 1 );
}
}
printf( "XXX: Pass check clauses! %d frames and %d clauses checked\n", k, counter );
return 1;
}
@ -149,7 +148,7 @@ Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
SeeAlso []
***********************************************************************/
sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k )
sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal )
{
sat_solver * pSat;
Vec_Ptr_t * vArrayK;
@ -165,7 +164,12 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k )
Vec_IntPush( p->vActVars, 0 );
// set the property output
Pdr_ManSetPropertyOutput( p, k );
if ( k < nTotal - 1 )
Pdr_ManSetPropertyOutput( p, k );
if (k == 0)
return pSat;
// add the clauses
Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
@ -194,7 +198,7 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses )
p->vClauses = vClauses;
for ( i = 0; i < Vec_VecSize(p->vClauses); ++i )
IPdr_ManSetSolver(p, i);
IPdr_ManSetSolver( p, i, Vec_VecSize( p->vClauses ) );
return 0;
}