From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 26 Aug 2013 22:56:39 +0000 (-0400)
Subject: bug 374 fix: assert litVal=desiredVal only for leaf nodes
X-Git-Tag: cvc5-1.0.0~7287^2~33^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3bc4d22bce9e3d882473cfe96f241f76a100aa9a;p=cvc5.git

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 de49f6e0a..78de1a74e 100644
--- 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 4bba7b049..42fedd480 100644
--- 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 \