From ba7b0392feed182939bed7b0247d8adf22e81520 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 14 Mar 2026 10:26:50 -0700
Subject: [PATCH] Add comments for regex enhancements in seq_model

Added comments regarding future improvements for regex handling.
---
 src/smt/seq/seq_model.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/seq/seq_model.cpp b/src/smt/seq/seq_model.cpp
index 2cbbf17ba..a13406201 100644
--- a/src/smt/seq/seq_model.cpp
+++ b/src/smt/seq/seq_model.cpp
@@ -272,6 +272,9 @@ namespace smt {
         return e ? expr_ref(e, m) : expr_ref(m);
     }
 
+    // NSB review: replace this by seq_rewriter::some_string_in_re when it is a regex over strings.
+    // add a routine that works for regular expressions over types other than strings to seq_rewriter
+    // use this for regexes over non-strings.
     expr_ref seq_model::generate_regex_witness(euf::snode* regex, unsigned depth) {
         if (!regex)
             return expr_ref(m_seq.str.mk_empty(m_seq.str.mk_string_sort()), m);