From 0659b7c7b50e49cbea1728f90f7ff04598f01eac Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 12 Jun 2012 17:33:29 +0000
Subject: cleanup of exit mechanism when decisionEngine is on\n\n fixes some
 bugs we were seeing in quantifiers+decision stuff

---
 src/prop/minisat/core/Solver.cc | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'src/prop')

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 697ab4853..9aefda75a 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1100,12 +1100,6 @@ lbool Solver::search(int nof_conflicts)
                 continue;
               } else {
                 // Yes, we're truly satisfiable
-		if(decisionEngineDone) {
-		  // but we might know that only because of decision engine
-		  Trace("decision") << decisionEngineDone << " decision engine stopping us" << std::endl;
-		  interrupt();
-		  return l_Undef;
-		}
                 return l_True;
               }
             } else if (check_type == CHECK_FINAL_FAKE) {
-- 
cgit v1.2.3