From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 13 Feb 2013 21:39:51 +0000 (-0500)
Subject: rm decision jh GiveUp related code
X-Git-Tag: cvc5-1.0.0~7407^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac53a61122c39c421ee7a8c10e2604ce468fc6f3;p=cvc5.git

rm decision jh GiveUp related code
---

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 46ec6f09f..6fb9c33ee 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -151,11 +151,6 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
   Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
 
   /* Good luck, hope you can get what you want */
-  // if(not (litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN)) {
-  //   Warning() << "WARNING: IMPORTANT: Please look into this. Sat solver is asking for a decision" << std::endl
-  //             << "when the assertion we are trying to justify is already unsat. OR there is a bug" << std::endl;
-  //   GiveUpException();
-  // }
   Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
          "invariant violated");