diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-08-26 19:53:14 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-08-26 19:53:14 +0000 |
| commit | 1857318ff8b072e07bc0a802960a7b87f119688d (patch) | |
| tree | ab8611efe47d95819ab77c2e0f0b2f1da614fcf1 /src/decision/justification_heuristic.cpp | |
| parent | 81f24e2d49dc9e598339304f3a72598d177f422c (diff) | |
minor, lying around in a wd (related to investigating bug 374)
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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 */ |