From 7e1fae418a766532f99cea06a1c6021268661864 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 May 2017 10:59:47 -0400
Subject: [PATCH] fix #1005, disable expansion of regular expression range to
 union as it degrades performance significantly

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp |  1 +
 src/smt/theory_arith.h            |  2 +-
 src/smt/theory_arith_aux.h        | 11 +++++++----
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 85d2ba749..7aa9329d4 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1434,6 +1434,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
  * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
  */
 br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
+    return BR_FAILED;
     TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
     zstring str_lo, str_hi;
     if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 439adbdff..cdc1a3933 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -505,7 +505,7 @@ namespace smt {
         struct var_value_eq {
             theory_arith & m_th;
             var_value_eq(theory_arith & th):m_th(th) {}
-            bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int(v1) == m_th.is_int(v2); }
+            bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int_src(v1) == m_th.is_int_src(v2); }
         };
 
         typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index de357c8d3..54b617152 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -2201,16 +2201,19 @@ namespace smt {
         int num       = get_num_vars();
         for (theory_var v = 0; v < num; v++) {
             enode * n        = get_enode(v);
-            TRACE("func_interp_bug", tout << "#" << n->get_owner_id() << " -> " << m_value[v] << "\n";);
-            if (!is_relevant_and_shared(n))
+            TRACE("func_interp_bug", tout << mk_pp(n->get_owner(), get_manager()) << " -> " << m_value[v] << " root #" << n->get_root()->get_owner_id() << " " << is_relevant_and_shared(n) << "\n";);
+            if (!is_relevant_and_shared(n)) {
                 continue;
+            }
             theory_var other = null_theory_var;
             other = m_var_value_table.insert_if_not_there(v);
-            if (other == v)
+            if (other == v) {
                 continue;
+            }
             enode * n2 = get_enode(other);
-            if (n->get_root() == n2->get_root())
+            if (n->get_root() == n2->get_root()) {
                 continue;
+            }
             TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
             m_assume_eq_candidates.push_back(std::make_pair(other, v));
             result = true;