diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 75014158a..ac0be651f 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 ) {