From dd6a11b526426579133d5920d9c9ed0c34ec3632 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Dec 2021 09:35:54 -0800
Subject: [PATCH] fix #5715

---
 src/smt/theory_seq.cpp | 32 +++++++++++++++++++++-----------
 src/smt/theory_seq.h   |  6 +++---
 2 files changed, 24 insertions(+), 14 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 369adccc1b5..5ef415d6a95 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -349,7 +349,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("propagate_contains");
         return FC_CONTINUE;
     }
-    if (fixed_length(true)) {
+    if (check_fixed_length(true, false)) {
         ++m_stats.m_fixed_length;
         TRACEFIN("zero_length");
         return FC_CONTINUE;
@@ -359,7 +359,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("split_based_on_length");
         return FC_CONTINUE;
     }
-    if (fixed_length()) {
+    if (check_fixed_length(false, false)) {
         ++m_stats.m_fixed_length;
         TRACEFIN("fixed_length");
         return FC_CONTINUE;
@@ -413,6 +413,11 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("branch_itos");
         return FC_CONTINUE;
     }
+    if (check_fixed_length(false, true)) {
+        ++m_stats.m_fixed_length;
+        TRACEFIN("fixed_length");
+        return FC_CONTINUE;
+    }
     if (m_unhandled_expr) {
         TRACEFIN("give_up");
         TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
@@ -461,18 +466,18 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & le
 }
 
 
-bool theory_seq::fixed_length(bool is_zero) {
+bool theory_seq::check_fixed_length(bool is_zero, bool check_long_strings) {
     bool found = false;    
     for (unsigned i = 0; i < m_length.size(); ++i) {
         expr* e = m_length.get(i);
-        if (fixed_length(e, is_zero)) {
+        if (fixed_length(e, is_zero, check_long_strings)) {
             found = true;
         }
     }
     return found;
 }
 
-bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
+bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings) {
     rational lo, hi;
     expr* e = nullptr;
     VERIFY(m_util.str.is_length(len_e, e));
@@ -493,12 +498,21 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
 
     expr_ref seq(e, m), head(m), tail(m);
 
+
+    TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
+    literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
+    if (ctx.get_assignment(a) == l_false)
+        return false;
+
+    if (!check_long_strings && lo > 20 && !is_zero)
+        return false;
+
     if (lo.is_zero()) {
         seq = m_util.str.mk_empty(e->get_sort());
     }
     else if (!is_zero) {
         unsigned _lo = lo.get_unsigned();
-        expr_ref_vector elems(m);        
+        expr_ref_vector elems(m);
         for (unsigned j = 0; j < _lo; ++j) {
             m_sk.decompose(seq, head, tail);
             elems.push_back(head);
@@ -506,10 +520,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
         }
         seq = mk_concat(elems.size(), elems.data());
     }
-    TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
-    literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
-    if (ctx.get_assignment(a) == l_false)
-        return false;
     literal b = mk_seq_eq(seq, e);
     if (ctx.get_assignment(b) == l_true)
         return false;
@@ -2873,7 +2883,7 @@ void theory_seq::add_axiom(literal_vector & lits) {
     for (literal lit : lits)
         ctx.mark_as_relevant(lit);
 
-    IF_VERBOSE(10, verbose_stream() << "ax ";
+    IF_VERBOSE(10, verbose_stream() << "ax";
                for (literal l : lits) ctx.display_literal_smt2(verbose_stream() << " ", l); 
                verbose_stream() << "\n");
     m_new_propagation = true;
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 68e9f3762a9..4b4c1d80bcb 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -243,7 +243,7 @@ namespace smt {
             replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {}
             ~replay_fixed_length() override {}
             void operator()(theory_seq& th) override {
-                th.fixed_length(m_e);
+                th.fixed_length(m_e, false, false);
                 m_e.reset();
             }
         };
@@ -436,8 +436,8 @@ namespace smt {
         bool check_length_coherence();
         bool check_length_coherence0(expr* e);
         bool check_length_coherence(expr* e);
-        bool fixed_length(bool is_zero = false);
-        bool fixed_length(expr* e, bool is_zero);
+        bool check_fixed_length(bool is_zero, bool check_long_strings);
+        bool fixed_length(expr* e, bool is_zero, bool check_long_strings);
         bool branch_variable_eq(depeq const& e);
         bool branch_binary_variable(depeq const& e);
         bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs);