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

Bug with in bmc3 when no 'sat' outputs are found and H != 0

This commit is contained in:
Alan Mishchenko 2013-10-08 23:21:28 -07:00
parent e0de796242
commit 62173b52ad
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/bmc/bmcBmc3.c
View File

@ -1321,6 +1321,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
p->pSat->nLearntMax = p->pSat->nLearntStart;
if ( pPars->fSolveAll && p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
if ( pPars->fVerbose )
{
Abc_Print( 1, "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n",