Commit 819b41bb by Alan Mishchenko

Fixed timeout problem in bmc3 -s.

parent 790ea654
...@@ -1392,6 +1392,13 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1392,6 +1392,13 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{ {
if ( i >= Saig_ManPoNum(pAig) ) if ( i >= Saig_ManPoNum(pAig) )
break; 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 // skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue; continue;
...@@ -1496,12 +1503,6 @@ clkOther += clock() - clk2; ...@@ -1496,12 +1503,6 @@ clkOther += clock() - clk2;
else else
{ {
assert( status == l_Undef ); 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 ) if ( pPars->nFramesJump )
{ {
pPars->nConfLimit = pPars->nConfLimitJump; pPars->nConfLimit = pPars->nConfLimitJump;
...@@ -1512,12 +1513,6 @@ clkOther += clock() - clk2; ...@@ -1512,12 +1513,6 @@ clkOther += clock() - clk2;
Saig_Bmc3ManStop( p ); Saig_Bmc3ManStop( p );
return RetValue; return RetValue;
} }
if ( pPars->nTimeOut && clock() > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut );
Saig_Bmc3ManStop( p );
return RetValue;
}
} }
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment