From 4cd4d16868b545becac4242f834aec6072c0e69d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 10 Jun 2026 18:20:49 +0000
Subject: [PATCH] Apply follow-up derive validation fixes

---
 src/ast/rewriter/seq_derive.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index ecc3df701..36d1ab560 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -438,7 +438,7 @@ namespace seq {
         else if (re().is_reverse(r, r1))
             result = r1;
         else if (re().is_concat(r, r1, r2))
-            result = mk_concat(mk_regex_reverse(r2), mk_regex_reverse(r1));
+            result = re().mk_concat(mk_regex_reverse(r2), mk_regex_reverse(r1));
         else if (m.is_ite(r, c, r1, r2))
             result = m.mk_ite(c, mk_regex_reverse(r1), mk_regex_reverse(r2));
         else if (re().is_union(r, r1, r2)) {
@@ -519,7 +519,8 @@ namespace seq {
             m_br.mk_not(is_nullable(r1), result);
         }
         else if (re().is_to_re(r, r1)) {
-            result = is_nullable(r1);
+            SASSERT(u().is_seq(r1->get_sort()));
+            result = m.mk_eq(u().str.mk_empty(r1->get_sort()), r1);
         }
         else if (m.is_ite(r, cond, r1, r2)) {
             m_br.mk_ite(cond, is_nullable(r1), is_nullable(r2), result);