1 files changed, 16 insertions, 4 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 54d2dee97..dc57fd5f9 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -47,7 +47,8 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
   d_curDecision(),
   d_curThreshold(0),
   d_childCache(uc),
-  d_weightCache(uc) {
+  d_weightCache(uc),
+  d_startIndexCache(c) {
   StatisticsRegistry::registerStat(&d_helfulness);
   StatisticsRegistry::registerStat(&d_giveup);
   StatisticsRegistry::registerStat(&d_timestat);
@@ -556,14 +557,22 @@ JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal)
     TNode curNode = getChildByWeight(node, i, desiredVal);
     if ( tryGetSatValue(curNode) != desiredValInverted ) {
       SearchResult ret = findSplitterRec(curNode, desiredVal);
-      if(ret != DONT_KNOW)
+      if(ret != DONT_KNOW) {
         return ret;
+      }
     }
   }
   Assert(d_curThreshold != 0, "handleAndOrEasy: No controlling input found");
   return DONT_KNOW;
 }
 
+int JustificationHeuristic::getStartIndex(TNode node) {
+  return d_startIndexCache[node];
+}
+void JustificationHeuristic::saveStartIndex(TNode node, int val) {
+  d_startIndexCache[node] = val;
+}
+
 JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node,
                                              SatValue desiredVal) {
   Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or 
@@ -571,11 +580,14 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNo
 
   int numChildren = node.getNumChildren();
   bool noSplitter = true;
-  for(int i = 0; i < numChildren; ++i) {
+  int i_st = getStartIndex(node);
+  for(int i = i_st; i < numChildren; ++i) {
     TNode curNode = getChildByWeight(node, i, desiredVal);
     SearchResult ret = findSplitterRec(curNode, desiredVal);
-    if (ret == FOUND_SPLITTER)
+    if (ret == FOUND_SPLITTER) {
+      if(i != i_st) saveStartIndex(node, i);
       return FOUND_SPLITTER;
+    }
     noSplitter = noSplitter && (ret == NO_SPLITTER);
   }
   return noSplitter ? NO_SPLITTER : DONT_KNOW;