Fix invalid sequence models for seq.foldl results observed through seq.nth (#10111)

`seq.foldl` could produce a concrete sequence model while related
`seq.nth` constraints were still validated against stale or
underconstrained length information, leading to invalid models. In the
reported case, `all` was modeled as `(seq.++ (seq.unit 7) (seq.unit 0))`
while `final = (seq.nth all 0)` remained inconsistent with `final = 6`.

- **Root cause**
- Sequence solutions were propagated as equalities, but parent `seq.len`
terms were not updated when a sequence term was solved.
- As a result, `seq.nth` guard reasoning could miss that a solved
sequence had known in-bounds length.

- **Solver change**
- Extend `theory_seq::add_solution` to collect parent `seq.len`
expressions of a solved term when the solved result is sequence-typed.
- After propagating the solved sequence equality, also propagate the
rewritten length equality for those parent length terms.
- Keep this propagation guarded to sequence results so scalar
`seq.foldl`/`seq.foldli` solutions do not regress from `sat` to
`unknown` under model validation.

- **Regression coverage**
  - Add a focused test for the reported SMT-LIB pattern:
    - `all = seq.foldl(...)`
    - `final = seq.nth all 0`
    - `initial = 0`
    - `final = 6`
- Add focused scalar `seq.foldl`/`seq.foldli` model-validation coverage
for the existing benchmark shapes that must continue returning `sat`.
- The regressions check both that model validation no longer reports an
invalid model for the `seq.nth` case and that scalar fold/foldi cases do
not regress to `unknown`.

- **Effect**
- Solved sequence terms now push enough derived length information for
dependent `seq.nth` constraints to validate against the actual modeled
sequence.
  - Existing scalar fold/foldi solving behavior is preserved.

```smt2
(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)
  (seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums)
)

(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))
(assert (= final (seq.nth all 0)))
(assert (= initial 0))
(assert (= final 6))
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

src/smt/theory_seq.cpp

@@ -1008,10 +1008,28 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps)  {
     m_rep.update(l, r, deps);
     enode* n1 = ensure_enode(l);
     enode* n2 = ensure_enode(r);    
+    ptr_vector<expr> len_parents;
+    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);
+    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;
 }
 
@@ -2640,14 +2658,14 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
         result = m_util.str.mk_foldli(e1, e2, e3, arg4);
         ctx.get_rewriter()(result);
     }
-#if 0
+    #if 0
     else if (m_util.str.is_nth_i(e, e1, e2)) {
         arg1 = try_expand(e1, deps);
         if (!arg1) return true;
         result = m_util.str.mk_nth_i(arg1, e2);
         // m_rewrite(result);
     }
-#endif
+    #endif
     else if (m_util.str.is_last_index(e, e1, e2)) {
         arg1 = try_expand(e1, deps);
         arg2 = try_expand(e2, deps);

src/test/seq_rewriter.cpp

@@ -23,14 +23,84 @@ Tests:
 #include "ast/reg_decl_plugins.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/seq_decl_plugin.h"
+#include "api/z3.h"
 #include "smt/smt_context.h"
+#include <cstring>
 #include <iostream>
+#include <sstream>
+#include <string>
 
 // Build a single-char string literal expression.
 static expr_ref mk_str(ast_manager& m, seq_util& su, unsigned c) {
     return expr_ref(su.str.mk_string(zstring(c)), m);
 }
 
+static void test_seq_foldl_nth_model_validation() {
+    Z3_context ctx = Z3_mk_context(nullptr);
+    char const* result =
+        Z3_eval_smtlib2_string(ctx,
+            "(set-option :model_validate true)\n"
+            "(declare-const initial Int)\n"
+            "(declare-const all (Seq Int))\n"
+            "(declare-const final Int)\n"
+            "(declare-const elements (Seq Int))\n"
+            "(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)\n"
+            "  (seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums))\n"
+            "(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))\n"
+            "(assert (= final (seq.nth all 0)))\n"
+            "(assert (= initial 0))\n"
+            "(assert (= final 6))\n"
+            "(check-sat)\n"
+            "(get-model)\n");
+    ENSURE(std::strstr(result, "sat") != nullptr);
+    ENSURE(std::strstr(result, "invalid model") == nullptr);
+    Z3_del_context(ctx);
+}
+
+static void test_seq_foldl_foldli_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, "invalid model") == nullptr);
+    unsigned sat_count = 0;
+    std::istringstream in{std::string(result)};
+    for (std::string line; std::getline(in, line);)
+        if (line == "sat")
+            ++sat_count;
+    ENSURE(sat_count == 4);
+    Z3_del_context(ctx);
+}
+
 void tst_seq_rewriter() {
     ast_manager m;
     reg_decl_plugins(m);
@@ -274,5 +344,8 @@ void tst_seq_rewriter() {
         }
     }
 
+    test_seq_foldl_nth_model_validation();
+    test_seq_foldl_foldli_scalar_model_validation();
+
     std::cout << "tst_seq_rewriter: all tests passed\n";
 }