From 5222f382af8c6d9174359da92f44abee4afa0331 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 8 Apr 2011 15:35:59 -0700
Subject: Adding SAT-solver-level timeouts to the BMC engines.

---
 src/sat/bsat/satSolver.c | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/sat/bsat/satSolver.c')

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index aa8c7f08..de186047 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1521,6 +1521,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
         }
+        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+            break;
     }
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
-- 
cgit v1.2.3