diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 0a3d83e7f9..a7dee69d93 100644
--- a/src/smt/theory_seq.cpp
+++ b/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);
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index 39036377f9..64adcfd107 100644
--- a/src/test/seq_rewriter.cpp
+++ b/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";
 }