From b60a44c66bb0fb9205334c38bce6c24c68261fe0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Apr 2026 10:33:28 -0700
Subject: [PATCH] classical

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_sgraph.cpp  | 2 ++
 src/smt/seq/seq_nielsen.cpp | 8 ++++----
 src/smt/seq_model.cpp       | 3 +++
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 3af0fa955..5768d7aec 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -132,6 +132,7 @@ namespace euf {
             n->m_nullable = false;
             n->m_level = 1;
             n->m_length = 1;
+            n->m_is_classical = false;
             break;
 
         case snode_kind::s_unit:
@@ -286,6 +287,7 @@ namespace euf {
 
         default:
             // NSB review: is this the correct defaults for unclassified nodes?
+            // Is this UNREACHABLE()?
             n->m_ground = true;
             n->m_regex_free = true;
             n->m_nullable = false;
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 357957449..684666f69 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -162,7 +162,7 @@ namespace seq {
     // -----------------------------------------------
 
     bool str_mem::is_primitive() const {
-        return m_str && m_str->length() == 1 && m_str->is_var();
+        return m_str && m_str->length() == 1 && m_str->is_var() && m_regex->is_ground();
     }
 
     bool str_mem::is_trivial() const {
@@ -2241,12 +2241,12 @@ namespace seq {
         // Priority 7: GPowerIntr - ground power introduction
         if (apply_gpower_intr(node))
             return ++m_stats.m_mod_gpower_intr, true;
-
-        // Priority 7b: Regex Factorization (Boolean Closure)
+        
+        // Priority 8: Regex Factorization (Boolean Closure)
         if (apply_regex_factorization(node))
             return ++m_stats.m_mod_regex_factorization, true;
 
-        // Priority 8: ConstNielsen - char vs var (2 children)
+        // Priority 8b: ConstNielsen - char vs var (2 children)
         if (apply_const_nielsen(node))
             return ++m_stats.m_mod_const_nielsen, true;
         
diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp
index 78b7e3f4a..660eaa4ad 100644
--- a/src/smt/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -30,6 +30,8 @@ namespace smt {
     {}
 
     void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen) {
+
+        TRACE(seq, nielsen.display(tout << nielsen.to_dot() << "\n"));
         m_var_values.reset();
         m_var_regex.reset();
         m_trail.reset();
@@ -50,6 +52,7 @@ namespace smt {
 
         // extract variable assignments from the satisfying leaf's substitution path
         extract_assignments(nielsen.sat_path());
+
     }
 
     model_value_proc* seq_model::mk_value(enode* n, model_generator& mg) {