diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-17 09:54:45 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-17 09:54:45 -0700 |
| commit | 819b41bb59b99b82e2c0391ce515d969ead585d7 (patch) | |
| tree | a6d58ab9115551c7013032fba85d942a090008dd /src/aig/saig | |
| parent | 790ea6545f5ed1bae248548038cde7901ee2361e (diff) | |
| download | abc-819b41bb59b99b82e2c0391ce515d969ead585d7.tar.gz abc-819b41bb59b99b82e2c0391ce515d969ead585d7.tar.bz2 abc-819b41bb59b99b82e2c0391ce515d969ead585d7.zip | |
Fixed timeout problem in bmc3 -s.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 75014158..ac0be651 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1392,6 +1392,13 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { if ( i >= Saig_ManPoNum(pAig) ) break; + // check for timeout + if ( pPars->nTimeOut && clock() > nTimeToStop ) + { + printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); + Saig_Bmc3ManStop( p ); + return RetValue; + } // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; @@ -1496,12 +1503,6 @@ clkOther += clock() - clk2; else { assert( status == l_Undef ); - if ( pPars->nTimeOut && clock() > nTimeToStop ) - { - printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); - Saig_Bmc3ManStop( p ); - return RetValue; - } if ( pPars->nFramesJump ) { pPars->nConfLimit = pPars->nConfLimitJump; @@ -1512,12 +1513,6 @@ clkOther += clock() - clk2; Saig_Bmc3ManStop( p ); return RetValue; } - if ( pPars->nTimeOut && clock() > nTimeToStop ) - { - printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); - Saig_Bmc3ManStop( p ); - return RetValue; - } } if ( pPars->fVerbose ) { |