diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-05-20 16:41:01 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-05-20 16:41:01 +0700 |
| commit | 38214f01c20227cfca6617c4b2ac55e090ec47fa (patch) | |
| tree | fca3c5fed8825492126ba14c50bfb21c3996b22c /src/aig/saig | |
| parent | 6ecc71f8f997cfdf182e356fa271051c87d41d78 (diff) | |
| download | abc-38214f01c20227cfca6617c4b2ac55e090ec47fa.tar.gz abc-38214f01c20227cfca6617c4b2ac55e090ec47fa.tar.bz2 abc-38214f01c20227cfca6617c4b2ac55e090ec47fa.zip | |
Do not allow quitting bmc3 after exploring 2^<num_ff> frames if jump-forward is enabled.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 2 |
1 files changed, 1 insertions, 1 deletions
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; |