From 38214f01c20227cfca6617c4b2ac55e090ec47fa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 20 May 2012 16:41:01 +0700 Subject: Do not allow quitting bmc3 after exploring 2^ frames if jump-forward is enabled. --- src/aig/saig/saigBmc3.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index b6558659..fb19783a 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1130,7 +1130,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) for ( f = 0; f < pPars->nFramesMax; f++ ) { // stop BMC after exploring all reachable states - if ( Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) + if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) { Saig_Bmc3ManStop( p ); return pPars->nFailOuts ? 0 : 1; -- cgit v1.2.3