diff options
Diffstat (limited to 'src')
| -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 ) { |