From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 14 Nov 2012 00:29:50 +0000 (+0000)
Subject: fix a race problem. due to interrupt mechanism minisat returned true instead of undef.
X-Git-Tag: cvc5-1.0.0~7603
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c6c93e0b65e67046ed654886b1294dcc6667687;p=cvc5.git

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 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");