From 10f5e944c99626d5f8e68aa874e43462569cabf7 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 6 Jun 2017 23:15:38 -0700 Subject: [PATCH] %pdra: fixed a bug --- src/base/wlc/wlcPth.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/base/wlc/wlcPth.c b/src/base/wlc/wlcPth.c index 7b8e19422..ddafab23c 100644 --- a/src/base/wlc/wlcPth.c +++ b/src/base/wlc/wlcPth.c @@ -40,7 +40,7 @@ ABC_NAMESPACE_IMPL_START extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig ); extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp ); -extern int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames ); +extern int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames, int RunId ); static volatile int g_nRunIds = 0; // the number of the last prover instance int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } @@ -119,7 +119,7 @@ void * Wla_Bmc3Thread ( void * pArg ) if ( pData->pWla->nIters > 1 && pData->RunId == g_nRunIds ) { - RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim ); + RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim, pData->RunId ); pData->pWla->iCexFrame += nFramesNoChangeLim; if ( RetValue == 1 )