From 0432311b116c7bdb9c7952e9cfada6808df752c6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Mar 2021 16:14:37 -0700
Subject: [PATCH] fix #5121

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

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index cd3e48fae..3b7c462fa 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1454,9 +1454,12 @@ bool theory_seq::internalize_term(app* term) {
     return true;
 }
 
-void theory_seq::add_length(expr* e, expr* l) {
+void theory_seq::add_length(expr* l) {
+    expr* e = nullptr;
+    VERIFY(m_util.str.is_length(l, e));
+    if (has_length(e))
+        return;
     TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
-    SASSERT(!m_has_length.contains(l));
     m_length.push_back(l);
     m_has_length.insert(e);
     m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
@@ -1504,7 +1507,7 @@ bool theory_seq::add_length_to_eqc(expr* e) {
         if (!has_length(o)) {
             expr_ref len(m_util.str.mk_length(o), m);
             ensure_enode(len);
-            add_length(o, len);
+            add_length(len);
             change = true;
         }
         n = n->get_next();
@@ -2471,6 +2474,7 @@ void theory_seq::enque_axiom(expr* e) {
 void theory_seq::deque_axiom(expr* n) {
     TRACE("seq", tout << "deque: " << mk_bounded_pp(n, m, 2) << "\n";);
     if (m_util.str.is_length(n)) {
+        add_length(n);
         m_ax.add_length_axiom(n);
         if (!ctx.at_base_level()) {
             m_trail_stack.push(push_replay(*this, alloc(replay_axiom, m, n)));
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 1041495af..6dbeddf41 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -555,7 +555,7 @@ namespace smt {
         void add_axiom(literal_vector& lits);
         
         bool has_length(expr *e) const { return m_has_length.contains(e); }
-        void add_length(expr* e, expr* l);
+        void add_length(expr* l);
         bool add_length_to_eqc(expr* n);
         bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
         void enforce_length_coherence(enode* n1, enode* n2);