From 1729232254340706ee07e10567888396bead7a29 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 May 2020 14:28:41 -0700
Subject: [PATCH] fix #4414

---
 src/smt/seq_unicode.cpp |  4 +++-
 src/smt/seq_unicode.h   |  2 +-
 src/smt/theory_seq.cpp  | 10 +++++-----
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/smt/seq_unicode.cpp b/src/smt/seq_unicode.cpp
index 4f293db46..7d36453be 100644
--- a/src/smt/seq_unicode.cpp
+++ b/src/smt/seq_unicode.cpp
@@ -71,7 +71,7 @@ namespace smt {
     }
 
     // != on characters
-    void seq_unicode::new_diseq_eh(theory_var v1, theory_var v2) {        
+    void seq_unicode::new_diseq_eh(theory_var v1, theory_var v2) {  
         adapt_eq(v1, v2);
     }
 
@@ -134,6 +134,7 @@ namespace smt {
     }
     
     void seq_unicode::propagate() {
+        return;
         ctx().push_trail(value_trail<smt::context, unsigned>(m_qhead));
         for (; m_qhead < m_asserted_edges.size() && !ctx().inconsistent(); ++m_qhead) {
             propagate(m_asserted_edges[m_qhead]);
@@ -141,6 +142,7 @@ namespace smt {
     }
     
     void seq_unicode::propagate(edge_id edge) {
+        return;
         if (dl.enable_edge(edge)) 
             return;
         dl.traverse_neg_cycle2(false, m_nc_functor);
diff --git a/src/smt/seq_unicode.h b/src/smt/seq_unicode.h
index 53a183e38..349b4cda5 100644
--- a/src/smt/seq_unicode.h
+++ b/src/smt/seq_unicode.h
@@ -70,12 +70,12 @@ namespace smt {
         var_value_hash   m_var_value_hash;
         var_value_eq     m_var_value_eq;
         var_value_table  m_var_value_table;
+        std::function<void(literal, literal, literal)> m_add_axiom;
 
         context& ctx() const { return th.get_context(); }
 
         void propagate(edge_id edge);
 
-        std::function<void(literal, literal, literal)> m_add_axiom;
         void add_axiom(literal a, literal b = null_literal, literal c = null_literal) {
             m_add_axiom(a, b, c);
         }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 06215f7d4..3bc033b25 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -377,7 +377,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("zero_length");
         return FC_CONTINUE;
     }
-    if (!m_unicode.final_check()) {
+    if (false && !m_unicode.final_check()) {
         return FC_CONTINUE;
     }
     if (get_fparams().m_split_w_len && len_based_split()) {
@@ -2510,7 +2510,7 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
 
 
 void theory_seq::propagate() {
-    m_unicode.propagate();
+    // m_unicode.propagate();
     while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
         expr_ref e(m);
         e = m_axioms[m_axioms_head].get();
@@ -3072,7 +3072,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
         // no-op
     }
-    else if (m_util.is_char_le(e, e1, e2)) {
+    else if (false && m_util.is_char_le(e, e1, e2)) {
         theory_var v1 = get_th_var(ctx.get_enode(e1));
         theory_var v2 = get_th_var(ctx.get_enode(e2));
         if (is_true) 
@@ -3093,7 +3093,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
 void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
     enode* n1 = get_enode(v1);
     enode* n2 = get_enode(v2);
-    if (m_util.is_char(n1->get_owner())) {
+    if (false && m_util.is_char(n1->get_owner())) {
         m_unicode.new_eq_eh(v1, v2);
         return;
     }
@@ -3188,7 +3188,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
             throw default_exception("convert regular expressions into automata");            
         }
     }
-    if (m_util.is_char(n1->get_owner())) {
+    if (false && m_util.is_char(n1->get_owner())) {
         m_unicode.new_diseq_eh(v1, v2);
         return;
     }