diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/abs/absIter.c | 2 | ||||
-rw-r--r-- | src/proof/abs/absOldRef.c | 2 | ||||
-rw-r--r-- | src/proof/ssw/sswRarity.c | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/abs/absIter.c b/src/proof/abs/absIter.c index 7b660359..ff14132d 100644 --- a/src/proof/abs/absIter.c +++ b/src/proof/abs/absIter.c @@ -58,7 +58,7 @@ int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 ) int nBTLimitAll = 0; int fVerbose = 0; int RetValue, iFrame; - RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1 ); + RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1, 0 ); assert( RetValue == 0 || RetValue == -1 ); Aig_ManStop( pAig ); Gia_ManStop( pAbs ); diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c index 315ecf89..1674f144 100644 --- a/src/proof/abs/absOldRef.c +++ b/src/proof/abs/absOldRef.c @@ -203,7 +203,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo } else { - Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 ); + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0, 0 ); } if ( pAbs->pSeqModel == NULL ) return NULL; diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index a02ea01b..1b7cab23 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -1011,7 +1011,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) if ( fTryBmc ) { Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits ); - Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 ); + Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0, 0 ); // if ( pNewAig->pSeqModel != NULL ) // Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail ); Aig_ManStop( pNewAig ); |