From 1c24c835c9e138f377e60ac50fb0a83b4145deaf Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 23 Mar 2026 13:20:06 -0700
Subject: [PATCH] Fix three assertion violations in nseq string solver (#9106)

- seq_model.cpp: skip trivial memberships in collect_var_regex_constraints;
  SAT leaf nodes can have "" in nullable_regex (trivial) in addition to
  primitive (single-variable) memberships after Brzozowski derivative
  consumption reduces a concrete string membership to empty.

- seq_nielsen.cpp: fix SASSERT(!var) typo in var_ub(); should be SASSERT(var)
  matching the pattern in var_lb().

- seq_regex.cpp: replace VERIFY(re_expr) with null guard in
  minterm_to_char_set(); nullptr means no regex constraint and should
  return the full alphabet, as the test test_minterm_nullptr_is_full expects.


Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/31db5346-9b60-4a20-a101-beca9fc9e4f8

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.cpp | 2 +-
 src/smt/seq/seq_regex.cpp   | 3 ++-
 src/smt/seq_model.cpp       | 2 ++
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 098f58518..810198963 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -310,7 +310,7 @@ namespace seq {
     }
 
     unsigned nielsen_node::var_ub(euf::snode* var) const {
-        SASSERT(!var);
+        SASSERT(var);
         unsigned v = UINT_MAX;
         m_var_ub.find(var->id(), v);
         return v;
diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp
index 0a8eca302..c0597bd51 100644
--- a/src/smt/seq/seq_regex.cpp
+++ b/src/smt/seq/seq_regex.cpp
@@ -1173,7 +1173,8 @@ namespace seq {
         seq_util& seq = m_sg.get_seq_util();
         unsigned max_c = seq.max_char();
 
-        VERIFY(re_expr);
+        if (!re_expr)
+            return char_set::full(max_c);
 
         // full_char: the whole alphabet [0, max_char]
         if (seq.re.is_full_char(re_expr))
diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp
index 724ac360d..256db7a91 100644
--- a/src/smt/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -324,6 +324,8 @@ namespace smt {
         SASSERT(sat_node);
         for (auto const& mem : sat_node->str_mems()) {
             SASSERT(mem.m_str && mem.m_regex);
+            if (mem.is_trivial())
+                continue; // empty string in nullable regex: already satisfied, no variable to constrain
             VERIFY(mem.is_primitive()); // everything else should have been eliminated already
             euf::snode* first = mem.m_str->first();
             unsigned id = first->id();