1 files changed, 13 insertions, 15 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 7d19d3363..b4fbe1cbd 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -163,12 +163,10 @@ inline void computeXorIffDesiredValues
   }
 }
 
-
-
-void JustificationHeuristic::addAssertions
-(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) {
+void JustificationHeuristic::addAssertions(
+    const preprocessing::AssertionPipeline &assertions)
+{
+  size_t assertionsEnd = assertions.getRealAssertionsEnd();
 
   Trace("decision")
     << "JustificationHeuristic::addAssertions()"
@@ -177,19 +175,19 @@ void JustificationHeuristic::addAssertions
     << std::endl;
 
   // Save the 'real' assertions locally
-  for(unsigned i = 0; i < assertionsEnd; ++i)
+  for (size_t i = 0; i < assertionsEnd; i++)
+  {
     d_assertions.push_back(assertions[i]);
+  }
 
   // Save mapping between ite skolems and ite assertions
-  for(IteSkolemMap::iterator i = iteSkolemMap.begin();
-      i != iteSkolemMap.end(); ++i) {
-
-    Trace("decision::jh::ite")
-      << " jh-ite: " << (i->first) << " maps to "
-      << assertions[(i->second)] << std::endl;
-    Assert(i->second >= assertionsEnd && i->second < assertions.size());
+  for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap())
+  {
+    Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to "
+                               << assertions[(i.second)] << std::endl;
+    Assert(i.second >= assertionsEnd && i.second < assertions.size());
 
-    d_iteAssertions[i->first] = assertions[i->second];
+    d_iteAssertions[i.first] = assertions[i.second];
   }
 
   // Automatic weight computation