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 9b4815fd4c5d7824c29beb250c8cd60f0090bc9c..8d36d9e05cb57df427092cc7ce1e7a151106fb37 100644 (file)
--- 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);
           }
         }
       }