From 38d725dc5a5ad96a9072b5891a80572943c5b5fe Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Thu, 9 Apr 2026 11:48:35 +0200
Subject: [PATCH] Deriving by allchar should not crash

---
 src/ast/euf/euf_sgraph.cpp | 10 +++++-----
 src/smt/theory_nseq.cpp    |  6 +++++-
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index cd975c328..6c904764b 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -559,9 +559,10 @@ namespace euf {
             if (ele_sort != elem_expr->get_sort()) {
                 // std::cout << "Different sorts: " << ele_sort->get_name() << " vs " << elem_expr->get_sort()->get_name() << std::endl;
                 expr* lo = nullptr, *hi = nullptr;
-                if (m_seq.re.is_full_char(elem_expr))
-                    return nullptr;
-                if (m_seq.re.is_range(elem_expr, lo, hi) && lo) {
+                if (m_seq.re.is_full_char(elem_expr)) {
+                    elem_expr = m_seq.str.mk_char(0);
+                }
+                else if (m_seq.re.is_range(elem_expr, lo, hi) && lo) {
                     expr* lo_ch = nullptr;
                     zstring zs;
                     if (m_seq.str.is_unit(lo, lo_ch))
@@ -579,8 +580,7 @@ namespace euf {
         }
         
         expr_ref result = m_rewriter.mk_derivative(elem_expr, re_expr);
-        if (!result)
-            return nullptr;
+        SASSERT(result);
         return mk(result);
     }
 
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 23fdbcd19..5a9e53ecb 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -687,6 +687,7 @@ namespace smt {
                 v.reset();
             }
         };
+        std::cout << "Nielsen assumptions:\n";
         ctx.push_trail(reset_vector(m_nielsen_literals));
         for (auto const& c : m_nielsen.sat_node()->constraints()) {
             bool was_internalized = ctx.e_internalized(c.fml);   
@@ -696,6 +697,7 @@ namespace smt {
             case l_true: 
                 break;
             case l_undef:
+                //std::cout << "Undef: " << mk_pp(c.fml, m) << "\n";
                 has_undef = true; 
                 ctx.force_phase(lit);                
                 IF_VERBOSE(2, verbose_stream() << 
@@ -708,10 +710,12 @@ namespace smt {
                                   << "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
                 ctx.force_phase(lit);
                 has_undef = true;
-                ctx.force_phase(lit);    
+                ctx.force_phase(lit);
+                //std::cout << "False: " << mk_pp(c.fml, m) << "\n";
                 break;
             }
         }
+        std::cout << std::endl;
         if (has_undef)
             return false;
         return true;