diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-30 13:53:18 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-30 13:53:18 -0700 |
| commit | 1cb140bb1143df405817ae62bde2dcd866fc282c (patch) | |
| tree | d964030340c4e659b9f5bf22c83b631691cbd277 /src | |
| parent | ecf91190d6a1dab0691ad03f42c816ec2788722b (diff) | |
| download | abc-1cb140bb1143df405817ae62bde2dcd866fc282c.tar.gz abc-1cb140bb1143df405817ae62bde2dcd866fc282c.tar.bz2 abc-1cb140bb1143df405817ae62bde2dcd866fc282c.zip | |
%pdra: fixed bugs
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 4 | ||||
| -rw-r--r-- | src/base/wlc/wlcPth.c | 6 | ||||
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 3 |
3 files changed, 8 insertions, 5 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index abc71809..aaf7f045 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1545,7 +1545,9 @@ void Wla_ManRefine( Wla_Man_t * pWla ) if ( pWla->fNewAbs ) { - assert( pWla->pCex == NULL ); + if ( pWla->pCex ) + Abc_CexFree( pWla->pCex ); + pWla->pCex = NULL; Gia_ManStop( pWla->pGia ); pWla->pGia = NULL; return; } diff --git a/src/base/wlc/wlcPth.c b/src/base/wlc/wlcPth.c index 5ce2ad0a..cc7b76d6 100644 --- a/src/base/wlc/wlcPth.c +++ b/src/base/wlc/wlcPth.c @@ -86,7 +86,7 @@ void * Wla_Bmc3Thread ( void * pArg ) { int status; int RetValue = -1; - int nFramesNoChangeLim = 3; + int nFramesNoChangeLim = 10; Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg; Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig ); Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars; @@ -94,7 +94,7 @@ void * Wla_Bmc3Thread ( void * pArg ) pBmcPars->pFuncStop = Wla_CallBackToStop; pBmcPars->RunId = pData->RunId; - if ( pData->pWla->nIters > 1 && pData->pWla->pPars->fShrinkAbs ) + if ( pData->pWla->pPars->fShrinkAbs ) pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim; RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 ); @@ -117,7 +117,7 @@ void * Wla_Bmc3Thread ( void * pArg ) if ( pData->RunId < g_nRunIds && pData->fVerbose ) Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId ); - if ( pData->RunId == g_nRunIds ) + if ( pData->pWla->nIters > 1 && pData->RunId == g_nRunIds ) { RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim ); pData->pWla->iCexFrame += nFramesNoChangeLim; diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 8cc964e5..c59bfe1c 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -160,7 +160,8 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p ) printf( "Cube[%d][%d] not inductive!\n", k, j ); } - assert( RetValue == 1 ); + if ( RetValue == -1 ) + return -1; } } |