From 8c6c93e0b65e67046ed654886b1294dcc6667687 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 14 Nov 2012 00:29:50 +0000
Subject: [PATCH] fix a race problem. due to interrupt mechanism minisat
 returned true instead of undef.

---
 src/prop/minisat/core/Solver.cc | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b5d524c31..ba36ac879 100644
--- 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");
 
-- 
2.30.2