From c18188cba87a369a759f232f84c2564755ab3365 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Apr 2026 05:44:53 +0200
Subject: [PATCH] avoid crashes in cases like wildcard-matching-regex-67.smt2,
 need regex constraint solving

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_nseq.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index a7ef85ced..9ea9fe874 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -656,6 +656,13 @@ namespace smt {
                 return FC_DONE;
             }
 
+            if (!has_eq_or_mem && has_unhandled_preds()) {
+                TRACE(seq, tout << "nielsen root if null\n");
+                // this can happen for regex constraint only benchmarks
+                // qf_s\20250410-matching\wildcard-matching-regex-67.smt2
+                return FC_GIVEUP;
+            }
+
             populate_nielsen_graph();
 
             // assert length constraints derived from string equalities
@@ -664,6 +671,8 @@ namespace smt {
                 return FC_CONTINUE;
             }
 
+            SASSERT(m_nielsen.root());            
+
             m_nielsen.assert_node_new_int_constraints(m_nielsen.root());
 
             ++m_num_final_checks;