From 0528c869058a2760e5c2d00dd207cbaf0283c881 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 26 Jul 2025 12:30:42 -0700
Subject: [PATCH] fix #7745

axioms for len(substr(...)) escaped due to nested rewriting
---
 src/ast/rewriter/seq_axioms.cpp | 29 ++++++++++++++++++++++++++---
 src/smt/theory_seq.cpp          |  6 ++----
 2 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index d9faaf4a6..621abd422 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1224,16 +1224,39 @@ namespace seq {
         let n = len(x)
         - len(a ++ b) = len(a) + len(b) if x = a ++ b
         - len(unit(u)) = 1              if x = unit(u)
+        - len(extract(x, o, l)) = l     if len(x) >= o + l etc
         - len(str) = str.length()       if x = str
         - len(empty) = 0                if x = empty
         - len(int.to.str(i)) >= 1       if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
         - len(x) >= 0                   otherwise
     */
     void axioms::length_axiom(expr* n) {
-        expr* x = nullptr;
+        expr* x = nullptr, * y = nullptr, * offs = nullptr, * l = nullptr;
         VERIFY(seq.str.is_length(n, x));
-        if (seq.str.is_concat(x) ||
-            seq.str.is_unit(x) ||
+        if (seq.str.is_concat(x) && to_app(x)->get_num_args() != 0) {
+            ptr_vector<expr> args;
+            for (auto arg : *to_app(x)) 
+                args.push_back(seq.str.mk_length(arg));
+            expr_ref len(a.mk_add(args), m);
+            add_clause(mk_eq(len, n));
+        }        
+        else if (seq.str.is_extract(x, y, offs, l)) {
+            // len(extract(y, o, l)) = l if len(y) >= o + l, o >= 0, l >= 0
+            // len(extract(y, o, l)) = 0 if o < 0 or l <= 0 or len(y) < o
+            // len(extract(y, o, l)) = o + l - len(y) if o <= len(y) < o + l
+            expr_ref len_y(mk_len(y), m);
+            expr_ref z(a.mk_int(0), m);
+            expr_ref y_ge_l(a.mk_ge(len_y, a.mk_add(offs, l)), m);
+            expr_ref y_ge_o(a.mk_ge(len_y, offs), m);
+            expr_ref offs_ge_0(a.mk_ge(offs, z), m);
+            expr_ref l_ge_0(a.mk_ge(l, z), m);
+            add_clause(~offs_ge_0, ~l_ge_0, ~y_ge_l, mk_eq(n, l));
+            add_clause(offs_ge_0, mk_eq(n, z));
+            add_clause(l_ge_0, mk_eq(n, z));
+            add_clause(y_ge_o, mk_eq(n, z));
+            add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(a.mk_add(offs, l), len_y)));  
+        }
+        else if (seq.str.is_unit(x) ||
             seq.str.is_empty(x) ||
             seq.str.is_string(x)) {
             expr_ref len(n, m);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index b7ecb4685..88e5b3ce5 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -439,7 +439,6 @@ final_check_status theory_seq::final_check_eh() {
 }
 
 
-
 bool theory_seq::set_empty(expr* x) {
     add_axiom(~mk_eq(m_autil.mk_int(0), mk_len(x), false), mk_eq_empty(x));
     return true;
@@ -475,9 +474,8 @@ 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, check_long_strings)) {
-            found = true;
-        }
+        if (fixed_length(e, is_zero, check_long_strings)) 
+            found = true;        
     }
     return found;
 }