diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-08 23:21:28 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-08 23:21:28 -0700 |
| commit | 62173b52ad03e8165ae106236e7ab1930c679d6e (patch) | |
| tree | fbdca05a0bc84425ffc187717653b6e10ed64b9c /src | |
| parent | e0de7962426e1d75c4e109d2589d305404bc3f77 (diff) | |
| download | abc-62173b52ad03e8165ae106236e7ab1930c679d6e.tar.gz abc-62173b52ad03e8165ae106236e7ab1930c679d6e.tar.bz2 abc-62173b52ad03e8165ae106236e7ab1930c679d6e.zip | |
Bug with in bmc3 when no 'sat' outputs are found and H != 0
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index a8604923..ed8f089a 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -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", |