rm decision jh GiveUp related code

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 46ec6f09fc3f96552d5b5d8149462f76ae496a87..6fb9c33ee96f981d4eaa62c8b5a0563a8b0ea331 100644 (file)
--- 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");