From 4f438adfde5031ade6e9a4df7668219ddc9d493d Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 15 Apr 2015 12:20:13 -0700
Subject: [PATCH] Fix for unconstrained bug.

---
 src/smt/smt_engine.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 25ac4c516..229cc7c7c 100644
--- 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);
   }
-- 
2.30.2