1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f72275cb2..4ed0bcb60 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -62,7 +62,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_inPreregister(false),
   d_preRegistrationVisitor(this, context),
-  d_sharedTermsVisitor(d_sharedTerms)
+  d_sharedTermsVisitor(d_sharedTerms),
+  d_unconstrainedSimp(context, logicInfo)
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     d_theoryTable[theoryId] = NULL;
@@ -1011,3 +1012,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion)
   result = Rewriter::rewrite(result);
   return result;
 }
+
+
+void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
+{
+  d_unconstrainedSimp.processAssertions(assertions);
+}