decision/ : save d_prvsIndex in JH

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index de6bf5095ce9c80b3f5aef49287b51e1d721d4ad..5d13d2dd2e777bbe001fbb7d184f01cb63d5c640 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -130,8 +130,10 @@ public:
         return prop::undefSatLiteral;
       }
 
-      if(litDecision != undefSatLiteral)
+      if(litDecision != undefSatLiteral) {
+        d_prvsIndex = i;
         return litDecision;
+      }
     }
 
     Trace("decision") << "jh: Nothing to split on " << std::endl;