From 61371b4abff56ef0ee9a789ff903c51842f71729 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Nov 2019 18:49:30 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 27 ++++++++++++++++++++++++++-
 src/smt/theory_seq.h   |  2 ++
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 53deab912..3a81f18ec 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3683,7 +3683,8 @@ bool theory_seq::internalize_term(app* term) {
         mk_var(e);
         return true;
     }
-    for (auto arg : *term) {
+    for (auto arg : *term) {        
+        ensure_enodes(arg);
         mk_var(ensure_enode(arg));
     }
     if (m.is_bool(term)) {
@@ -5117,6 +5118,29 @@ enode* theory_seq::ensure_enode(expr* e) {
     return n;
 }
 
+void theory_seq::ensure_enodes(expr* e) {
+    if (!m_ensure_todo.empty()) return;
+    context& ctx = get_context();
+    if (ctx.e_internalized(e)) return;
+    m_ensure_todo.push_back(e);
+    expr_mark visited;
+    for (unsigned i = 0; i < m_ensure_todo.size(); ++i) {
+        e = m_ensure_todo[i];
+        if (is_app(e) && to_app(e)->get_family_id() == m_util.get_family_id()) {
+            for (expr* arg : *to_app(e)) {
+                if (!ctx.e_internalized(arg) && !visited.is_marked(arg)) {
+                    m_ensure_todo.push_back(arg);
+                    visited.mark(arg);
+                }
+            }
+        }
+    }	
+    for (unsigned i = m_ensure_todo.size(); i-- > 0; ) {
+        ensure_enode(m_ensure_todo[i]);
+    }
+    m_ensure_todo.reset();
+}
+
 template <class T>
 static T* get_th_arith(context& ctx, theory_id afid, expr* e) {
     theory* th = ctx.get_theory(afid);
@@ -5430,6 +5454,7 @@ void theory_seq::add_at_axiom(expr* e) {
         unsigned k = iv.get_unsigned();
         for (unsigned j = 0; j <= k; ++j) {
             es.push_back(m_util.str.mk_unit(mk_nth(s, m_autil.mk_int(j))));
+            ensure_enode(es.back());
         }
         nth = es.back();
         es.push_back(mk_skolem(m_tail, s, i));
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 1cdc33694..5760e6f82 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -629,6 +629,8 @@ namespace smt {
         expr_ref mk_add(expr* a, expr* b);
         expr_ref mk_len(expr* s);
         enode* ensure_enode(expr* a);
+        ptr_vector<expr> m_ensure_todo;
+        void ensure_enodes(expr* e);
         enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
         dependency* mk_join(dependency* deps, literal lit);
         dependency* mk_join(dependency* deps, literal_vector const& lits);