From 891b2e6c8ef5c0e5b93f238c37a2279eff9ac537 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 14 Mar 2026 23:17:32 +0000
Subject: [PATCH] Address code review feedback: improve null-sort handling in
 seq_model and some_seq_in_re

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 7 +++++--
 src/smt/seq_model.cpp             | 1 +
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d90e31c11..f3aed58ec 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -6016,7 +6016,9 @@ void seq_rewriter::op_cache::cleanup() {
 
 lbool seq_rewriter::some_seq_in_re(expr* r, expr_ref& result) {
     sort* seq_sort = nullptr;
-    if (u().is_re(r, seq_sort) && u().is_string(seq_sort)) {
+    if (!u().is_re(r, seq_sort))
+        return l_undef;
+    if (u().is_string(seq_sort)) {
         zstring s;
         lbool res = some_string_in_re(r, s);
         if (res == l_true)
@@ -6024,9 +6026,10 @@ lbool seq_rewriter::some_seq_in_re(expr* r, expr_ref& result) {
         return res;
     }
     // For non-string sequences: check if the regex accepts the empty sequence.
+    SASSERT(seq_sort);
     expr_ref is_null = is_nullable(r);
     if (m().is_true(is_null)) {
-        result = str().mk_empty(seq_sort ? seq_sort : str().mk_string_sort());
+        result = str().mk_empty(seq_sort);
         return l_true;
     }
     return l_undef;
diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp
index 8de5a7f5a..ed10c531d 100644
--- a/src/smt/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -233,6 +233,7 @@ namespace smt {
             // Build the repeated string: base^exp_val
             if (exp_val.is_zero()) {
                 sort* srt = n->get_sort();
+                SASSERT(srt);
                 if (!srt) srt = m_seq.str.mk_string_sort();
                 return expr_ref(m_seq.str.mk_empty(srt), m);
             }