bug 374 fix: assert litVal=desiredVal only for leaf nodes

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index de49f6e0a7442db1f9640447fc8e8046b0f2131a..78de1a74e5ae68bfb4d2ba9a79cd4c2b31dd0d9a 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -96,7 +96,8 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
     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);
+    // Commenting out. See bug 374. In short, to do with how CNF stream works.
+    // Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
 
     SatValue desiredVal = SAT_VALUE_TRUE;
     SatLiteral litDecision;
@@ -105,6 +106,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
 
     if(litDecision != undefSatLiteral) {
       setPrvsIndex(i);
+      Trace("decision") << "jh: spliting on " << litDecision << std::endl;
       return litDecision;
     }
   }
@@ -441,8 +443,9 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
   Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
 
   /* Good luck, hope you can get what you want */
-  Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
-         "invariant violated");
+  // See bug 374
+  // Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
+  //       "invariant violated");
 
   /* What type of node is this */
   Kind k = node.getKind();     
@@ -458,12 +461,12 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
    * If not in theory of booleans, check if this is something to split-on.
    */
   if(tId != theory::THEORY_BOOL) {
-
     // if node has embedded ites, resolve that first
     if(handleEmbeddedITEs(node) == FOUND_SPLITTER)
       return FOUND_SPLITTER;
 
     if(litVal != SAT_VALUE_UNKNOWN) {
+      Assert(litVal == desiredVal);
       setJustified(node);
       return NO_SPLITTER;
     } 

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 4bba7b0493316ce51d6436ae4157b925f1c9c1c8..42fedd480369447063e7ab0414cdb3f54c8ad007 100644 (file)
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -27,6 +27,8 @@ TESTS =       \
        uflia-xs-09-16-3-4-1-5.delta03.smt \
        aufbv-fuzz01.smt \
        bug347.smt \
+       bug374a.smt \
+       bug374b.smt2 \
        error20.smt \
        error20.delta01.smt \
        error122.smt \
@@ -54,6 +56,8 @@ EXTRA_DIST = $(TESTS) \
        quant-Arrays_Q1-noinfer.smt2.expect \
        wchains010ue.delta02.smt.expect \
        bug347.smt.expect \
+       bug374a.smt.expect \
+       bug374b.smt2.expect \
        quant-ex1.disable_miniscope.smt2.expect \
        wchains010ue.smt.expect \
        just_sat.expect \