From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 26 Aug 2012 19:53:14 +0000 (+0000)
Subject: minor, lying around in a wd (related to investigating bug 374)
X-Git-Tag: cvc5-1.0.0~7842
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1857318ff8b072e07bc0a802960a7b87f119688d;p=cvc5.git

minor, lying around in a wd (related to investigating bug 374)
---

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index c7051d570..67000b1ba 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -164,7 +164,12 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
   Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
 
   /* Good luck, hope you can get what you want */
-  Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, 
+  // 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");
 
   /* What type of node is this */
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index f0ae9fe78..6d9493e89 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -111,13 +111,18 @@ public:
     }
 
     for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
-      Debug("decision") << d_assertions[i] << std::endl;
+      Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl;
 
       // Sanity check: if it was false, aren't we inconsistent?
       Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
 
       SatValue desiredVal = SAT_VALUE_TRUE;
-      SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal);
+      SatLiteral litDecision;
+      try {
+        litDecision = findSplitter(d_assertions[i], desiredVal);
+      }catch(GiveUpException &e) {
+        return prop::undefSatLiteral;
+      }
 
       if(litDecision != undefSatLiteral)
         return litDecision;
@@ -180,11 +185,7 @@ private:
   {
     bool ret;
     SatLiteral litDecision;
-    try {
-      ret = findSplitterRec(node, desiredVal, &litDecision);
-    }catch(GiveUpException &e) {
-      return prop::undefSatLiteral;
-    }
+    ret = findSplitterRec(node, desiredVal, &litDecision);
     if(ret == true) {
       Debug("decision") << "Yippee!!" << std::endl;
       //d_prvsIndex = i;