From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 15 Apr 2015 19:20:13 +0000 (-0700)
Subject: Fix for unconstrained bug.
X-Git-Tag: cvc5-1.0.0~6357
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f438adfde5031ade6e9a4df7668219ddc9d493d;p=cvc5.git

Fix for unconstrained bug.
---

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);
   }