From bc9d35567f37e33a5c630052529eabf97ae6bc26 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 13 Jul 2026 21:39:40 +0000
Subject: [PATCH] Guard seq length propagation for foldl

---
 src/smt/theory_seq.cpp    | 28 ++++++++++++++++------------
 src/test/seq_rewriter.cpp | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3dfd156128..c613f1cc7b 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1001,22 +1001,26 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps)  {
     enode* n1 = ensure_enode(l);
     enode* n2 = ensure_enode(r);    
     ptr_vector<expr> len_parents;
-    auto collect_len_parents = [&](enode* n) {
-        for (enode* p : n->get_parents()) {
-            if (m_util.str.is_length(p->get_expr()))
-                len_parents.push_back(p->get_expr());
-        }
-    };
-    collect_len_parents(n1);
-    collect_len_parents(n2);
+    if (m_util.is_seq(r)) {
+        auto collect_len_parents = [&](enode* n) {
+            for (enode* p : n->get_parents()) {
+                if (m_util.str.is_length(p->get_expr()))
+                    len_parents.push_back(p->get_expr());
+            }
+        };
+        collect_len_parents(n1);
+        collect_len_parents(n2);
+    }
     TRACE(seq, tout << mk_bounded_pp(l, m, 2) << " ==> " << mk_bounded_pp(r, m, 2) << "\n"; display_deps(tout, deps);
           tout << "#" << n1->get_owner_id() << " ==> #" << n2->get_owner_id() << "\n";
           tout << (n1->get_root() == n2->get_root()) << "\n";);         
     propagate_eq(deps, n1, n2);
-    expr_ref len_r(m_util.str.mk_length(r), m);
-    m_rewrite(len_r);
-    for (expr* len_e : len_parents) {
-        propagate_eq(deps, len_e, len_r, false);
+    if (m_util.is_seq(r)) {
+        expr_ref len_r(m_util.str.mk_length(r), m);
+        m_rewrite(len_r);
+        for (expr* len_e : len_parents) {
+            propagate_eq(deps, len_e, len_r, false);
+        }
     }
     return true;
 }
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index dc248a27f3..378911838f 100644
--- a/src/test/seq_rewriter.cpp
+++ b/src/test/seq_rewriter.cpp
@@ -54,6 +54,44 @@ static void test_seq_foldl_nth_model_validation() {
     Z3_del_context(ctx);
 }
 
+static void test_seq_foldl_scalar_model_validation() {
+    Z3_context ctx = Z3_mk_context(nullptr);
+    char const* result =
+        Z3_eval_smtlib2_string(ctx,
+            "(set-option :model_validate true)\n"
+            "(push)\n"
+            "(declare-fun f (Int Int) Int)\n"
+            "(declare-const il (Seq Int))\n"
+            "(assert (= (seq.foldl f 0 il) 5))\n"
+            "(check-sat)\n"
+            "(pop)\n"
+            "(push)\n"
+            "(declare-const il (Seq Int))\n"
+            "(declare-const F (Array Bool Int Bool))\n"
+            "(assert (= (seq.foldl F true il) true))\n"
+            "(assert (> (seq.len il) 0))\n"
+            "(assert (not (= F ((as const (Array Bool Int Bool)) true))))\n"
+            "(check-sat)\n"
+            "(pop)\n"
+            "(push)\n"
+            "(declare-fun f (Int Int Int) Int)\n"
+            "(declare-const il (Seq Int))\n"
+            "(assert (= (seq.foldli f 0 0 il) 5))\n"
+            "(check-sat)\n"
+            "(pop)\n"
+            "(push)\n"
+            "(declare-const il (Seq Int))\n"
+            "(declare-const F (Array Int Bool Int Bool))\n"
+            "(assert (= (seq.foldli F 5 true il) true))\n"
+            "(assert (> (seq.len il) 0))\n"
+            "(assert (not (= F ((as const (Array Int Bool Int Bool)) true))))\n"
+            "(check-sat)\n"
+            "(pop)\n");
+    ENSURE(std::strstr(result, "unknown") == nullptr);
+    ENSURE(std::strstr(result, "sat\nsat\nsat\nsat") != nullptr);
+    Z3_del_context(ctx);
+}
+
 void tst_seq_rewriter() {
     ast_manager m;
     reg_decl_plugins(m);
@@ -78,6 +116,7 @@ void tst_seq_rewriter() {
         rw(e);
         std::cout << "empty range lo>hi: " << mk_pp(e, m) << "\n";
         ENSURE(su.re.is_empty(e));
+        test_seq_foldl_scalar_model_validation();
     }
 
     // -----------------------------------------------------------------------