diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-16 13:33:43 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-16 13:33:43 -0800 |
| commit | 4dc7eb6f734c003c212690e6c66c4711428a8f9c (patch) | |
| tree | 1b09747c0ef7665c90c1d44f40bf30b3aedc0e44 | |
| parent | fd0ff0171eced62f11f9cbe67570d09e6dd22065 (diff) | |
| download | abc-4dc7eb6f734c003c212690e6c66c4711428a8f9c.tar.gz abc-4dc7eb6f734c003c212690e6c66c4711428a8f9c.tar.bz2 abc-4dc7eb6f734c003c212690e6c66c4711428a8f9c.zip | |
Added 'gap timeout' to bmc3 and sim3.
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 1185e84d..72e091ca 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -975,6 +975,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); // perform simulation rounds + timeLastSolved = clock(); for ( r = 0; !nRounds || (nNumRestart * nRestart + r < nRounds); r++ ) { clk = clock(); diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 98689ff8..28752d1b 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1349,6 +1349,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); // perform frames Aig_ManRandom( 1 ); + pPars->timeLastSolved = clock(); for ( f = 0; f < pPars->nFramesMax; f++ ) { // stop BMC after exploring all reachable states |