diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-13 16:39:51 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 18:19:52 -0500 |
| commit | ac53a61122c39c421ee7a8c10e2604ce468fc6f3 (patch) | |
| tree | c3a835dd4f3c59bd49d800c8c263ca669e283994 /src/decision | |
| parent | d389114bc99897fc7ea3c744194225ebab368851 (diff) | |
rm decision jh GiveUp related code
Diffstat (limited to 'src/decision')
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 46ec6f09f..6fb9c33ee 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -151,11 +151,6 @@ bool JustificationHeuristic::findSplitterRec(TNode node, Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); /* Good luck, hope you can get what you want */ - // 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"); |