diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-12 17:33:29 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-12 17:33:29 +0000 |
| commit | 0659b7c7b50e49cbea1728f90f7ff04598f01eac (patch) | |
| tree | c0f2ab0f6734fa6c78c68857c1a2c2d551f7a644 /src/prop | |
| parent | 43dd3569232fd72d7791db7dd113bdff0bdf916d (diff) | |
cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we were seeing in quantifiers+decision stuff
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 6 |
1 files changed, 0 insertions, 6 deletions
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) { |