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

Bug fix in bmc3.

This commit is contained in:
Alan Mishchenko 2012-09-17 17:39:42 -07:00
parent 1f9abfd7a8
commit 6dc3a0a246
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/aig/saig/saigBmc3.c
View File

@ -1240,12 +1240,17 @@ int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
***********************************************************************/
int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
{
int Lit;
// perform terminary simulation
int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
if ( Value != SAIG_TER_UND )
return (int)(Value == SAIG_TER_ONE);
// construct CNF if value is ternary
return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
Lit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
// extend the SAT solver
if ( p->nSatVars > sat_solver_nvars(p->pSat) )
sat_solver_setnvars( p->pSat, p->nSatVars );
return Lit;
}