summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/saig/saigBmc3.c19
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 )
{