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)

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index cd69eeb743acde588d88e3f6902e10d9e28e8582..93ff65e6dc265fe466c5c58f27d1fd5220dcde21 100644 (file)
--- 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