Commit 4dc7eb6f by Alan Mishchenko

Added 'gap timeout' to bmc3 and sim3.

parent fd0ff017
...@@ -975,6 +975,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in ...@@ -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 ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
// perform simulation rounds // perform simulation rounds
timeLastSolved = clock();
for ( r = 0; !nRounds || (nNumRestart * nRestart + r < nRounds); r++ ) for ( r = 0; !nRounds || (nNumRestart * nRestart + r < nRounds); r++ )
{ {
clk = clock(); clk = clock();
......
...@@ -1349,6 +1349,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) ...@@ -1349,6 +1349,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
// perform frames // perform frames
Aig_ManRandom( 1 ); Aig_ManRandom( 1 );
pPars->timeLastSolved = clock();
for ( f = 0; f < pPars->nFramesMax; f++ ) for ( f = 0; f < pPars->nFramesMax; f++ )
{ {
// stop BMC after exploring all reachable states // stop BMC after exploring all reachable states
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment