(proof-new) Preprocessing passes use proper interfaces to assertions pipeline (#5164)

This PR eliminates all uses of assertions pipeline that are not proper, which two-fold:
(1) The assertion list should never be modified in a custom way (without going through replace / push_back),
(2) Places where an assertion is "conjoined" to an existing spot in the vector should use conjoin instead of replace.
This is required for proper proof generation.

This fixes CVC4/cvc4-projects#75.

1 files changed, 7 insertions, 7 deletions

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 504814e07..971288b67 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -339,8 +339,7 @@ bool ProcessAssertions::apply(Assertions& as)
       // assertion
       IteSkolemMap::iterator it = iskMap.begin();
       IteSkolemMap::iterator iend = iskMap.end();
-      NodeBuilder<> builder(AND);
-      builder << assertions[assertions.getRealAssertionsEnd() - 1];
+      std::vector<Node> newConj;
       vector<TNode> toErase;
       for (; it != iend; ++it)
       {
@@ -367,19 +366,20 @@ bool ProcessAssertions::apply(Assertions& as)
           }
         }
         // Move this iteExpr into the main assertions
-        builder << assertions[(*it).second];
-        assertions[(*it).second] = d_true;
+        newConj.push_back(assertions[(*it).second]);
+        assertions.replace((*it).second, d_true);
         toErase.push_back((*it).first);
       }
-      if (builder.getNumChildren() > 1)
+      if (!newConj.empty())
       {
         while (!toErase.empty())
         {
           iskMap.erase(toErase.back());
           toErase.pop_back();
         }
-        assertions[assertions.getRealAssertionsEnd() - 1] =
-            Rewriter::rewrite(Node(builder));
+        size_t index = assertions.getRealAssertionsEnd() - 1;
+        Node newAssertion = NodeManager::currentNM()->mkAnd(newConj);
+        assertions.conjoin(index, newAssertion);
       }
       // TODO(b/1256): For some reason this is needed for some benchmarks, such
       // as