From e63992c8bd99ce0fbc1c76575646387f8411c216 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 24 Jul 2020 15:46:54 -0700
Subject: [PATCH] fix #4589

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 4 +++-
 src/ast/seq_decl_plugin.cpp      | 7 ++++++-
 src/smt/seq_axioms.cpp           | 6 +++++-
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 4f40adfe8..7754ad031 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -679,6 +679,7 @@ namespace datatype {
     bool util::is_recursive_core(sort* s) const {
         obj_map<sort, status> already_found;
         ptr_vector<sort> todo, subsorts;
+        sort* s0 = s;
         todo.push_back(s);
         status st;
         while (!todo.empty()) {
@@ -700,7 +701,8 @@ namespace datatype {
                         if (is_datatype(s2)) {
                             if (already_found.find(s2, st)) {
                                 // type is recursive
-                                if (st == GRAY) return true;
+                                if (st == GRAY && s0 == s2) 
+                                    return true;
                             }
                             else {
                                 todo.push_back(s2);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index a3759e6e7..9764ba18c 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1285,13 +1285,18 @@ unsigned seq_util::str::min_length(expr* s) const {
 unsigned seq_util::str::max_length(expr* s) const {
     SASSERT(u.is_seq(s));
     unsigned result = 0;
-    expr* s1 = nullptr, *s2 = nullptr;
+    expr* s1 = nullptr, *s2 = nullptr, *s3 = nullptr;
+    unsigned n = 0;
     zstring st;
     auto get_length = [&](expr* s1) {
         if (is_empty(s1))
             return 0u;
         else if (is_unit(s1))
             return 1u;
+        else if (is_at(s1))
+            return 1u;
+        else if (is_extract(s1, s1, s2, s3)) 
+            return (arith_util(m).is_unsigned(s3, n)) ? n : UINT_MAX;
         else if (is_string(s1, st))
             return st.length();
         else
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 48203105e..0acc9ba51 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -252,10 +252,14 @@ void seq_axioms::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
   s = "" or !contains(x*s1, s)
 */
 void seq_axioms::tightest_prefix(expr* s, expr* x) {
+    literal s_eq_emp = mk_eq_empty(s);
+    if (seq.str.max_length(s) <= 1) {
+        add_axiom(s_eq_emp, ~mk_literal(seq.str.mk_contains(x, s)));
+        return;
+    }
     expr_ref s1 = m_sk.mk_first(s);
     expr_ref c  = m_sk.mk_last(s);
     expr_ref s1c = mk_concat(s1, seq.str.mk_unit(c));
-    literal s_eq_emp = mk_eq_empty(s);
     add_axiom(s_eq_emp, mk_seq_eq(s, s1c));
     add_axiom(s_eq_emp, ~mk_literal(seq.str.mk_contains(mk_concat(x, s1), s)));
 }