Use skolem lemma in prop layer interfaces (#7320)

2 files changed, 10 insertions, 14 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 97e56c58c..c7ec46337 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -47,19 +47,17 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
-    std::vector<TrustNode> newAsserts;
-    std::vector<Node> newSkolems;
-    TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
+    std::vector<SkolemLemma> newAsserts;
+    TrustNode trn = pe->removeItes(assertion, newAsserts);
     if (!trn.isNull())
     {
       // process
       assertions->replaceTrusted(i, trn);
     }
-    Assert(newSkolems.size() == newAsserts.size());
-    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    for (const SkolemLemma& lem : newAsserts)
     {
-      imap[assertions->size()] = newSkolems[j];
-      assertions->pushBackTrusted(newAsserts[j]);
+      imap[assertions->size()] = lem.d_skolem;
+      assertions->pushBackTrusted(lem.d_lemma);
     }
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 641cab162..2f9d12637 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -44,19 +44,17 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
-    std::vector<TrustNode> newAsserts;
-    std::vector<Node> newSkolems;
-    TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
+    std::vector<SkolemLemma> newAsserts;
+    TrustNode trn = propEngine->preprocess(assertion, newAsserts);
     if (!trn.isNull())
     {
       // process
       assertions->replaceTrusted(i, trn);
     }
-    Assert(newSkolems.size() == newAsserts.size());
-    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    for (const SkolemLemma& lem : newAsserts)
     {
-      imap[assertions->size()] = newSkolems[j];
-      assertions->pushBackTrusted(newAsserts[j]);
+      imap[assertions->size()] = lem.d_skolem;
+      assertions->pushBackTrusted(lem.d_lemma);
     }
   }