diff options
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 891d89cc5..c9a6b7e1b 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -108,6 +108,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D if(litDecision != undefSatLiteral) { setPrvsIndex(i); Trace("decision") << "jh: splitting on " << litDecision << std::endl; + ++d_helfulness; return litDecision; } } @@ -197,9 +198,7 @@ SatLiteral JustificationHeuristic::findSplitter(TNode node, SatValue desiredVal) { d_curDecision = undefSatLiteral; - if(findSplitterRec(node, desiredVal)) { - ++d_helfulness; - } + findSplitterRec(node, desiredVal); return d_curDecision; } |