From 393d567aa6dc22cb3f4b858d84201cf7920c872d Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 13 Jun 2015 10:21:40 -0700
Subject: [PATCH] Fix for assertion failure: smt_engine.cpp:1992:
 Rewriter::rewrite(d_assertions[i]) == d_assertions[i] when --ite-simp and
 --repeat-simp are on

---
 src/theory/theory_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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