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 c7051d57065d2b97d2a4b655e4e9afa94f2a7bb9..67000b1ba37fca7d85f21cad76e3a9497de2350b 100644 (file)
--- 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 f0ae9fe78e3b7f84c86174814ce08158c131e9b8..6d9493e890f4020dce535d5f1d857851ae3e586b 100644 (file)
--- 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;