1 files changed, 19 insertions, 1 deletions
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index af66c2a2a..15f5d3eb0 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -16,6 +16,8 @@
 
 #include "preprocessing_pass_context.h"
 
+#include "expr/node_algorithm.h"
+
 namespace CVC4 {
 namespace preprocessing {
 
@@ -27,7 +29,8 @@ PreprocessingPassContext::PreprocessingPassContext(
     : d_smt(smt),
       d_resourceManager(resourceManager),
       d_iteRemover(iteRemover),
-      d_circuitPropagator(circuitPropagator)
+      d_circuitPropagator(circuitPropagator),
+      d_symsInAssertions(smt->d_userContext)
 {
 }
 
@@ -43,5 +46,20 @@ void PreprocessingPassContext::enableIntegers()
   req.enableIntegers();
 }
 
+void PreprocessingPassContext::recordSymbolsInAssertions(
+    const std::vector<Node>& assertions)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<Node, NodeHashFunction> syms;
+  for (TNode cn : assertions)
+  {
+    expr::getSymbols(cn, syms, visited);
+  }
+  for (const Node& s : syms)
+  {
+    d_symsInAssertions.insert(s);
+  }
+}
+
 }  // namespace preprocessing
 }  // namespace CVC4