summaryrefslogtreecommitdiffstats
path: root/src/aig/int
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-10-31 14:59:47 -0500
committerAlan Mishchenko <alanmi@berkeley.edu>2011-10-31 14:59:47 -0500
commit868a1b9aeb2bf825a68c37c530107efe72d50d5d (patch)
tree872e030d59ce89d595812f1c8ae4e776905d3112 /src/aig/int
parentf08be2742e892b7b81f234785cbbae85c61ab024 (diff)
downloadabc-868a1b9aeb2bf825a68c37c530107efe72d50d5d.tar.gz
abc-868a1b9aeb2bf825a68c37c530107efe72d50d5d.tar.bz2
abc-868a1b9aeb2bf825a68c37c530107efe72d50d5d.zip
Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.
Diffstat (limited to 'src/aig/int')
-rw-r--r--src/aig/int/intCore.c10
1 files changed, 3 insertions, 7 deletions
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index d6295931..0cd5eb36 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -81,11 +81,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
Inter_Check_t * pCheck = NULL;
Aig_Man_t * pAigTemp;
int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
- int nTimeNewOut = 0;
-
- // set runtime limit
- if ( pPars->nSecLimit )
- nTimeNewOut = clock() + pPars->nSecLimit * CLOCKS_PER_SEC;
+ int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
// sanity checks
assert( Saig_ManRegNum(pAig) > 0 );
@@ -252,7 +248,7 @@ p->timeCnf += clock() - clk;
}
else if ( RetValue == -1 )
{
- if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
+ if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out
{
if ( pPars->fVerbose )
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
@@ -331,7 +327,7 @@ p->timeEqu += clock() - clk - timeTemp;
Inter_CheckStop( pCheck );
return 1;
}
- if ( pPars->nSecLimit && clock() > nTimeNewOut )
+ if ( pPars->nSecLimit && time(NULL) > nTimeNewOut )
{
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
p->timeTotal = clock() - clkTotal;