From 17d67c1b50ae29120e4bedff8beaec13f191057f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Dec 2019 20:14:35 -0800
Subject: [PATCH] fix #2726

---
 src/smt/theory_seq.cpp | 24 +++++++++++++++++++++---
 src/smt/theory_seq.h   |  2 ++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 411a365f3..47196d4dc 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -288,6 +288,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     m_autil(m),
     m_arith_value(m),
     m_trail_stack(*this),
+    m_internalize_depth(0),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
     m_res(m),
@@ -3681,6 +3682,13 @@ bool theory_seq::internalize_term(app* term) {
         mk_var(e);
         return true;
     }
+    flet<unsigned> _depth(m_internalize_depth, m_internalize_depth+1);
+
+    if (m_internalize_depth > 50 && m_ensure_todo.empty()) {
+        ensure_enodes(term);
+        return true;
+    }
+
     for (auto arg : *term) {        
         mk_var(ensure_enode(arg));
     }
@@ -5115,6 +5123,14 @@ enode* theory_seq::ensure_enode(expr* e) {
     return n;
 }
 
+struct theory_seq::compare_depth {
+    bool operator()(expr* a, expr* b) const {
+        unsigned d1 = get_depth(a);
+        unsigned d2 = get_depth(b);
+        return d1 < d2 || (d1 == d2 && a->get_id() < b->get_id());
+    }
+};
+
 void theory_seq::ensure_enodes(expr* e) {
     if (!m_ensure_todo.empty()) return;
     context& ctx = get_context();
@@ -5132,9 +5148,11 @@ void theory_seq::ensure_enodes(expr* e) {
             }
         }
     }	
-    // TBD: std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), compare_depth);
-    for (unsigned i = m_ensure_todo.size(); i-- > 0; ) {
-        ensure_enode(m_ensure_todo[i]);
+    compare_depth cd;
+    std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), cd);
+
+    for (expr* e : m_ensure_todo) {
+        ensure_enode(e);
     }
     m_ensure_todo.reset();
 }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 5760e6f82..63efdeef2 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -51,6 +51,7 @@ namespace smt {
 
         class seq_value_proc;
         struct validate_model_proc;
+        struct compare_depth;
         
         // cache to track evaluations under equalities
         class eval_cache {
@@ -383,6 +384,7 @@ namespace smt {
         symbol           m_tail, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
         symbol           m_pre, m_post, m_eq, m_seq_align;
         ptr_vector<expr> m_todo;
+        unsigned         m_internalize_depth;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
 
         // maintain automata with regular expressions.