Evil bitvector preprocessing pass for simplifying powers of two.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6b7bf424f..ab805a6c5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -89,6 +89,7 @@
 #include "printer/options.h"
 
 #include "theory/arith/pseudoboolean_proc.h"
+#include "theory/bv/bvintropow2.h"
 
 using namespace std;
 using namespace CVC4;
@@ -2926,6 +2927,10 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess);
   }
 
+  if(options::bvIntroducePow2()){
+    theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess);
+  }
+
   dumpAssertions("pre-substitution", d_assertionsToPreprocess);
 
   // Apply the substitutions we already have, and normalize