From 50095be5ac2c1b9830a74c87fd0d8e2edc8b8438 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 May 2013 19:58:25 -0700 Subject: Adding runtime limit per output to multi-output DPR (pdr -H ). --- src/sat/bmc/bmcBmc3.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/sat/bmc') 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 -- cgit v1.2.3