Fix for unconstrained bug.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 25ac4c5163347e29083b4649314b835c5a3cdeb9..229cc7c7cf6a42f2ac682b513ce834350c23f7bb 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3119,6 +3119,9 @@ void SmtEnginePrivate::processAssertions() {
   if(options::unconstrainedSimp()) {
     dumpAssertions("pre-unconstrained-simp", d_assertions);
     Chat() << "...doing unconstrained simplification..." << endl;
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
+    }
     unconstrainedSimp();
     dumpAssertions("post-unconstrained-simp", d_assertions);
   }