diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 13f2732d8..fd379fd2d 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -41,7 +41,6 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
         opt_DeferEQCConsistencyCheck(false),
         opt_CheckVariableScope(true),
         opt_ConcatOverlapAvoid(true),
-        opt_DeferredSearchOrder(true),
         /* Internal setup */
         search_started(false),
         m_autil(m),
@@ -900,8 +899,7 @@ bool theory_str::can_propagate() {
             || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty()
             || !m_axiom_Substr_todo.empty() || !m_axiom_Replace_todo.empty()
 			|| !m_axiom_RegexIn_todo.empty() || !m_library_aware_axiom_todo.empty()
-			|| !m_delayed_axiom_setup_terms.empty()
-            || (opt_DeferredSearchOrder && !m_new_eqs.empty())
+			|| !m_delayed_axiom_setup_terms.empty();
             ;
 }
 
@@ -1002,14 +1000,6 @@ void theory_str::propagate() {
             set_up_axioms(m_delayed_axiom_setup_terms[i].get());
         }
         m_delayed_axiom_setup_terms.reset();
-
-        if (opt_DeferredSearchOrder) {
-            for (unsigned i = 0; i < m_new_eqs.size(); ++i) {
-                var_pair & p = m_new_eqs[i];
-                cb_new_eq(p.first, p.second);
-            }
-            m_new_eqs.reset();
-        }
     }
 }
 
@@ -7072,15 +7062,7 @@ void theory_str::init_search_eh() {
     search_started = true;
 }
 
-void theory_str::new_eq_eh(theory_var v1, theory_var v2) {
-    if (opt_DeferredSearchOrder) {
-        m_new_eqs.push_back(var_pair(v1,v2));
-    } else {
-        cb_new_eq(v1, v2);
-    }
-}
-
-void theory_str::cb_new_eq(theory_var x, theory_var y) {
+void theory_str::new_eq_eh(theory_var x, theory_var y) {
     //TRACE("t_str_detail", tout << "new eq: v#" << x << " = v#" << y << std::endl;);
     TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
                                   mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 598e9d8c9..7f1e1dd9c 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -97,8 +97,6 @@ namespace smt {
         }
     };
 
-    typedef std::pair<theory_var, theory_var> var_pair;
-
     class theory_str : public theory {
         struct T_cut
         {
@@ -190,16 +188,6 @@ namespace smt {
          */
         bool opt_ConcatOverlapAvoid;
 
-        /*
-         * If DeferredSearchOrder is set to true,
-         * certain behaviours from user_smt_theory will be emulated in order to
-         * reproduce more faithfully the search order used by Z3str2.
-         * In particular, new equalities will be saved and processed during propagate(),
-         * and asserted axioms will be deferred until the end of each propagate() step.
-         */
-        bool opt_DeferredSearchOrder;
-        svector<var_pair> m_new_eqs;
-
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;
@@ -597,11 +585,9 @@ namespace smt {
         void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet);
         bool propagate_length_within_eqc(expr * var);
 
+        // TESTING
         void refresh_theory_var(expr * e);
 
-        // user_smt_theory search order emulation
-        void cb_new_eq(theory_var v1, theory_var v2);
-
     public:
         theory_str(ast_manager & m, theory_str_params const & params);
         virtual ~theory_str();