summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcBmc3.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-05-03 19:58:25 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-05-03 19:58:25 -0700
commit50095be5ac2c1b9830a74c87fd0d8e2edc8b8438 (patch)
tree06e61100033466fac89fadda0eeb22dff338c8bf /src/sat/bmc/bmcBmc3.c
parenta59968ce8c55618ca7c84972faacba31c591a39f (diff)
downloadabc-50095be5ac2c1b9830a74c87fd0d8e2edc8b8438.tar.gz
abc-50095be5ac2c1b9830a74c87fd0d8e2edc8b8438.tar.bz2
abc-50095be5ac2c1b9830a74c87fd0d8e2edc8b8438.zip
Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
-rw-r--r--src/sat/bmc/bmcBmc3.c4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 96fff2af..424e08c9 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1393,10 +1393,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, k, Lit, status;
clock_t clk, clk2, clkOther = 0, clkTotal = clock();
- clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne;
+ clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
clock_t nTimeToStopNG, nTimeToStop;
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
+ if ( pPars->nTimeOutOne && !pPars->fSolveAll )
+ pPars->nTimeOutOne = 0;
nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager