Bug fix in justification heuristic. Had to do with how

a "visited" node in the recursive findSplitter method was
handled (which would lead to infinite loop). Earlier,
they were ignored assuming the ancestor would split on it
later. The right thing to do is to split on it right away.

(Fixes errors from the fuzzer, not the ones from last night's
regression)

1 files changed, 16 insertions, 1 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index cd69eeb74..93ff65e6d 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -141,8 +141,23 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
   }
 
   /* Base case */
-  if (checkJustified(node) || d_visited.find(node) != d_visited.end())
+  if (checkJustified(node))
     return false;
+  if(d_visited.find(node) != d_visited.end()) {
+
+    if(tryGetSatValue(node) != SAT_VALUE_UNKNOWN) {
+      setJustified(node);
+      return false;
+    } else {
+      Assert(d_decisionEngine->hasSatLiteral(node));
+      SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
+      *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
+      Trace("decision") << "decision " << *litDecision << std::endl;
+      Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
+      return true;
+    }
+
+  }
 
 #if defined CVC4_ASSERTIONS || defined CVC4_TRACING
   // We don't always have a sat literal, so remember that. Will need