5 files changed, 30 insertions, 22 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 6ebd73a5f..ec8943f4a 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -113,8 +113,9 @@ SatValue DecisionEngine::getPolarity(SatVariable var)
   }
 }
 
-void DecisionEngine::addAssertions(
-    const preprocessing::AssertionPipeline& assertions)
+void DecisionEngine::addAssertions(const std::vector<Node>& assertions,
+                                   const std::vector<Node>& ppLemmas,
+                                   const std::vector<Node>& ppSkolems)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
@@ -126,7 +127,7 @@ void DecisionEngine::addAssertions(
 
   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
   {
-    d_needIteSkolemMap[i]->addAssertions(assertions);
+    d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems);
   }
 }
 
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 52e1e2d1a..afa16397d 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -24,7 +24,6 @@
 #include "base/output.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat_solver_types.h"
@@ -142,9 +141,12 @@ class DecisionEngine {
   // External World helping us help the Strategies
 
   /**
-   * Add a list of assertions from an AssertionPipeline.
+   * Add a list of assertions, as well as lemmas coming from preprocessing
+   * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
    */
-  void addAssertions(const preprocessing::AssertionPipeline& assertions);
+  void addAssertions(const std::vector<Node>& assertions,
+                     const std::vector<Node>& ppLemmas,
+                     const std::vector<Node>& ppSkolems);
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index f7c28299d..ebddc659d 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -19,7 +19,9 @@
 #ifndef CVC4__DECISION__DECISION_STRATEGY_H
 #define CVC4__DECISION__DECISION_STRATEGY_H
 
-#include "preprocessing/assertion_pipeline.h"
+#include <vector>
+
+#include "expr/node.h"
 #include "prop/sat_solver_types.h"
 #include "smt/term_formula_removal.h"
 
@@ -58,8 +60,13 @@ public:
 
   bool needIteSkolemMap() override { return true; }
 
-  virtual void addAssertions(
-      const preprocessing::AssertionPipeline& assertions) = 0;
+  /**
+   * Add a list of assertions, as well as lemmas coming from preprocessing
+   * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
+   */
+  virtual void addAssertions(const std::vector<Node>& assertions,
+                             const std::vector<Node>& ppLemmas,
+                             const std::vector<Node>& ppSkolems) = 0;
 };/* class ITEDecisionStrategy */
 
 class RelevancyStrategy : public ITEDecisionStrategy {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index baf0056e9..afbff18c1 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -164,15 +164,14 @@ inline void computeXorIffDesiredValues
   }
 }
 
-void JustificationHeuristic::addAssertions(
-    const preprocessing::AssertionPipeline &assertions)
+void JustificationHeuristic::addAssertions(const std::vector<Node>& assertions,
+                                           const std::vector<Node>& ppLemmas,
+                                           const std::vector<Node>& ppSkolems)
 {
-  size_t assertionsEnd = assertions.getRealAssertionsEnd();
-
+  Assert(ppSkolems.size() == ppLemmas.size());
   Trace("decision")
     << "JustificationHeuristic::addAssertions()"
     << " size = " << assertions.size()
-    << " assertionsEnd = " << assertionsEnd
     << std::endl;
 
   // Save all assertions locally, including the assertions generated by term
@@ -198,13 +197,11 @@ void JustificationHeuristic::addAssertions(
   }
 
   // Save mapping between ite skolems and ite assertions
-  for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap())
+  for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++)
   {
-    Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to "
-                               << assertions[(i.second)] << std::endl;
-    Assert(i.second >= assertionsEnd && i.second < assertions.size());
-
-    d_skolemAssertions[i.first] = assertions[i.second];
+    Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to "
+                               << ppLemmas[i] << std::endl;
+    d_skolemAssertions[ppSkolems[i]] = ppLemmas[i];
   }
 
   // Automatic weight computation
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 5ecb5eb08..81b08f1a6 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -121,8 +121,9 @@ public:
 
   prop::SatLiteral getNext(bool &stopSearch) override;
 
-  void addAssertions(
-      const preprocessing::AssertionPipeline &assertions) override;
+  void addAssertions(const std::vector<Node>& assertions,
+                     const std::vector<Node>& ppLemmas,
+                     const std::vector<Node>& ppSkolems) override;
 
  private:
   /* getNext with an option to specify threshold */