From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 13 Jun 2015 17:21:40 +0000 (-0700)
Subject: Fix for assertion failure:
X-Git-Tag: cvc5-1.0.0~6282
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=393d567aa6dc22cb3f4b858d84201cf7920c872d;p=cvc5.git

Fix for assertion failure:
smt_engine.cpp:1992: Rewriter::rewrite(d_assertions[i]) == d_assertions[i]
when --ite-simp and --repeat-simp are on
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9b4815fd4..8d36d9e05 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1589,7 +1589,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
           if(curr != res){
             Node more = aiteu.reduceConstantIteByGCD(res);
             Debug("arith::ite::red") << "  gcd->" << more << endl;
-            assertions[i] = more;
+            assertions[i] = Rewriter::rewrite(more);
           }
         }
       }