fix a race problem. due to interrupt mechanism minisat returned true instead of undef.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b5d524c31a6d34ebb77720251773433af3e2679c..ba36ac8797605c2abb7a893226bc570ee3c57e2d 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1250,6 +1250,9 @@ lbool Solver::solve_()
         curr_restarts++;
     }
 
+    if(!withinBudget())
+        status = l_Undef;
+
     if (verbosity >= 1)
         printf("===============================================================================\n");