From e5ca451a0270f56c3961d719abf896fac8ea4244 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 4 Dec 2019 16:42:28 -0500
Subject: [PATCH] z3str3: remove unused str_eq_todo worklist

---
 src/smt/theory_str.cpp | 14 +++-----------
 src/smt/theory_str.h   |  1 -
 2 files changed, 3 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index f304539f5..f20ec4d3c 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -842,7 +842,7 @@ namespace smt {
     }
 
     bool theory_str::can_propagate() {
-        return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty()
+        return !m_basicstr_axiom_todo.empty()
             || !m_concat_axiom_todo.empty() || !m_concat_eval_todo.empty()
             || !m_library_aware_axiom_todo.empty()
             || !m_delayed_axiom_setup_terms.empty()
@@ -873,13 +873,6 @@ namespace smt {
             m_basicstr_axiom_todo.reset();
             TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;);
 
-            for (auto const& pair : m_str_eq_todo) {
-                enode * lhs = pair.first;
-                enode * rhs = pair.second;
-                handle_equality(lhs->get_owner(), rhs->get_owner());
-            }
-            m_str_eq_todo.reset();
-
             for (auto const& el : m_concat_axiom_todo) {
                 instantiate_concat_axiom(el);
             }
@@ -2136,7 +2129,6 @@ namespace smt {
         m_trail_stack.reset();
 
         m_basicstr_axiom_todo.reset();
-        m_str_eq_todo.reset();
         m_concat_axiom_todo.reset();
         pop_scope_eh(get_context().get_scope_level());
     }
@@ -3842,7 +3834,7 @@ namespace smt {
 
                     if (m_params.m_StrongArrangements) {
                         expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
-                        assert_axiom(ax_strong);
+                        assert_axiom_rw(ax_strong);
                     } else {
                         assert_implication(ax_l, ax_r);
                     }
@@ -3919,7 +3911,7 @@ namespace smt {
 
                 if (m_params.m_StrongArrangements) {
                     expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
-                    assert_axiom(ax_strong);
+                    assert_axiom_rw(ax_strong);
                 } else {
                     assert_implication(ax_l, ax_r);
                 }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 0852d6644..7218ee77b 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -328,7 +328,6 @@ protected:
     expr_ref_vector m_delayed_axiom_setup_terms;
 
     ptr_vector<enode> m_basicstr_axiom_todo;
-    svector<std::pair<enode*,enode*> > m_str_eq_todo;
     ptr_vector<enode> m_concat_axiom_todo;
     ptr_vector<enode> m_string_constant_length_todo;
     ptr_vector<enode> m_concat_eval_todo;