diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-08-26 18:56:39 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-08-26 19:01:34 -0400 |
| commit | 3bc4d22bce9e3d882473cfe96f241f76a100aa9a (patch) | |
| tree | dd4d65d88280974db2d7be5e8868fad2cd4e9bfd | |
| parent | 92fe124ecd014a9cc36abc684d055fc0b9ebca08 (diff) | |
bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.x
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 11 | ||||
| -rw-r--r-- | test/regress/regress0/decision/Makefile.am | 4 |
2 files changed, 11 insertions, 4 deletions
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 \ |