From 824ba1497744f0c646d4a6d9056b2d3108828854 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 4 Nov 2016 13:39:53 +0000
Subject: [PATCH] Disabled some ITE rewrite rules that were applied by default,
 but too expensive. Added re-computation of subterm occurrences in
 ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks).

---
 src/ast/rewriter/bool_rewriter.cpp      | 36 +++++++++++++------------
 src/tactic/core/ctx_simplify_tactic.cpp |  2 ++
 2 files changed, 21 insertions(+), 17 deletions(-)

diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index a914d6a0a..ce3eb5844 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -594,25 +594,27 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
         }
         return BR_DONE;
     }
-    if (m().is_value(t)) {
-        if (val == t) {
-            result = m().mk_or(cond, m().mk_eq(val, e));
+    if (m_ite_extra_rules) {
+        if (m().is_value(t)) {
+            if (val == t) {
+                result = m().mk_or(cond, m().mk_eq(val, e));
+            }
+            else {
+                mk_not(cond, result);
+                result = m().mk_and(result, m().mk_eq(val, e));
+            }
+            return BR_REWRITE2;
         }
-        else {
-            mk_not(cond, result);
-            result = m().mk_and(result, m().mk_eq(val, e));
+        if (m().is_value(e)) {
+            if (val == e) {
+                mk_not(cond, result);
+                result = m().mk_or(result, m().mk_eq(val, t));
+            }
+            else {
+                result = m().mk_and(cond, m().mk_eq(val, t));
+            }
+            return BR_REWRITE2;
         }
-        return BR_REWRITE2;
-    }
-    if (m().is_value(e)) {
-        if (val == e) {
-            mk_not(cond, result);
-            result = m().mk_or(result, m().mk_eq(val, t));
-        }
-        else {
-            result = m().mk_and(cond, m().mk_eq(val, t));
-        }
-        return BR_REWRITE2;
     }
     expr* cond2, *t2, *e2;
     if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 5258f8c5c..3e2790fe3 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -538,6 +538,8 @@ struct ctx_simplify_tactic::imp {
         }
         pop(scope_level() - old_lvl);
 
+        m_occs(g);
+
         // go backwards
         sz = g.size();
         for (unsigned i = sz; !g.inconsistent() && i > 0; ) {