1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 442b1ef1c..6f965879d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -119,7 +119,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
-  d_unconstrainedSimp(context, logicInfo)
+  d_unconstrainedSimp(context, logicInfo),
+  d_bvToBoolPreprocessor()
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     d_theoryTable[theoryId] = NULL;
@@ -1276,6 +1277,12 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   }
 }
 
+Node TheoryEngine::ppBvToBool(TNode assertion) {
+  Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion);
+  result = Rewriter::rewrite(result);
+  return result; 
+}
+
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
   Node result = d_iteSimplifier.simpITE(assertion);