Adding SAT-solver-level timeouts to the BMC engines.

2 files changed, 10 insertions, 2 deletions

diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 8e537142..1fc5a11a 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -767,7 +767,9 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
             nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
     } 
-
+    // set runtime limit
+    if ( nTimeOut )
+        sat_solver_set_runtime_limit( p->pSat, clock() + nTimeOut * CLOCKS_PER_SEC );
     for ( Iter = 0; ; Iter++ )
     {
         clk2 = clock();
@@ -841,8 +843,10 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
             printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
         else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
             printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else
+        else if ( nTimeOut == 0 || nTimeOut > clock() )
             printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        else
+            printf( "Reached timeout (%d sec).\n", nTimeOut );
     }
     Saig_BmcManStop( p );
     return Status;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 570e8a26..e038d7a0 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1054,6 +1054,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
             pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
     } 
+    // set runtime limit
+    if ( p->pPars->nTimeOut )
+        sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
+    // perform frames
     for ( f = 0; f < pPars->nFramesMax; f++ )
     {
         pPars->iFrame = f;