diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-03 19:58:25 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-03 19:58:25 -0700 |
commit | 50095be5ac2c1b9830a74c87fd0d8e2edc8b8438 (patch) | |
tree | 06e61100033466fac89fadda0eeb22dff338c8bf /src/sat/bmc | |
parent | a59968ce8c55618ca7c84972faacba31c591a39f (diff) | |
download | abc-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')
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 4 |
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 |