From 18f3ed1fb81a3ab168474af9467543dea44c7926 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 14 Oct 2014 11:50:24 -0400
Subject: [PATCH] trace decision-node

---
 src/decision/justification_heuristic.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 84f4d5074..72dea907c 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -477,7 +477,10 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
         return DONT_KNOW;
       SatVariable v =
         d_decisionEngine->getSatLiteral(node).getSatVariable();
-      d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
+      d_curDecision = SatLiteral(v, /* negated = */ desiredVal != SAT_VALUE_TRUE );
+      Trace("decision-node") << "[decision-node] requesting split on " << d_curDecision
+                             << ", node: " << node
+                             << ", polarity: " << (desiredVal ? "true" : "false") << std::endl;
       return FOUND_SPLITTER;
     }
   }
-- 
2.30.2