From c05c5caab523278606b0d5cb439614f446caa7b2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Mar 2021 18:07:00 -0700
Subject: [PATCH] fix #5111

---
 src/smt/theory_seq.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index e04c11d21..506191c6b 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1503,7 +1503,7 @@ bool theory_seq::add_length_to_eqc(expr* e) {
         expr* o = n->get_expr();
         if (!has_length(o)) {
             expr_ref len(m_util.str.mk_length(o), m);
-            enque_axiom(len);
+            ensure_enode(len);
             add_length(o, len);
             change = true;
         }
@@ -3028,6 +3028,7 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_from_code(n) ||
         m_util.str.is_to_code(n) ||
         m_util.str.is_unit(n) ||
+        m_util.str.is_length(n) || 
         m_util.str.is_le(n)) {
         enque_axiom(n);
     }