From 78fc27358e6b6aae27b11528be54003022b1f663 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 30 Jan 2013 11:59:59 -0500 Subject: [PATCH] decision/ : save d_prvsIndex in JH --- src/decision/justification_heuristic.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index de6bf5095..5d13d2dd2 100644 --- 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; -- 2.30.2