Fixed crasb if regex is reported SAT by pre-check

src/smt/seq/seq_nielsen.h

@@ -783,7 +783,7 @@ namespace seq {
 
         // Regex membership module: stabilizers, emptiness checks, language
         // inclusion, derivatives. Allocated in the constructor; owned by this graph.
-        seq::seq_regex*              m_seq_regex = nullptr;
+        seq_regex*              m_seq_regex = nullptr;
 
         // -----------------------------------------------
         // Modification counter for substitution length tracking.
@@ -835,6 +835,8 @@ namespace seq {
         nielsen_node* root() const { return m_root; }
         void set_root(nielsen_node* n) { m_root = n; }
 
+        void set_sat_node(nielsen_node* n) { m_sat_node = n; }
+
         // satisfying leaf node (set by solve() when result is sat)
         nielsen_node* sat_node() const { return m_sat_node; }
         // path of edges from root to sat_node (set when sat_node is set)

src/smt/seq_model.cpp

@@ -30,7 +30,7 @@ namespace smt {
         : m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_trail(m)
     {}
 
-    void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen, seq_state const& state) {
+    void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen) {
         m_var_values.reset();
         m_var_regex.reset();
         m_trail.reset();
@@ -41,7 +41,9 @@ namespace smt {
         mg.register_factory(m_factory);
 
         register_existing_values(nielsen);
-        collect_var_regex_constraints(nielsen.sat_node());
+        seq::nielsen_node* sat_node = nielsen.sat_node();
+        SASSERT(sat_node); // in case we report sat, this has to point to a satisfied Nielsen node!
+        collect_var_regex_constraints(sat_node);
 
         // solve integer constraints from the sat_path FIRST so that
         // m_int_model is available when snode_to_value evaluates power exponents

src/smt/seq_model.h

@@ -75,7 +75,7 @@ namespace smt {
         // Allocates seq_factory, registers it with mg, collects
         // existing string literals, and extracts variable assignments
         // from the satisfying Nielsen leaf node.
-        void init(model_generator& mg, seq::nielsen_graph& nielsen, seq_state const& state);
+        void init(model_generator& mg, seq::nielsen_graph& nielsen);
 
         // Phase 2: build a model_value_proc for the given enode.
         // Returns nullptr if the enode is not a sequence/string sort.

src/smt/theory_nseq.cpp

@@ -393,8 +393,7 @@ namespace smt {
         // emptiness for each variable's regex constraints.  This handles     
         // regex-only problems that the DFS cannot efficiently solve.
         if (get_fparams().m_nseq_regex_precheck) {
-            lbool precheck = check_regex_memberships_precheck();
+            switch (check_regex_memberships_precheck()) {
-            switch (precheck) { 
             case l_true:
                 // conflict was asserted inside check_regex_memberships_precheck
                 IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck UNSAT\n";);
@@ -402,6 +401,7 @@ namespace smt {
             case l_false:
                 // all regex constraints satisfiable, no word eqs/diseqs → SAT
                 IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";);
+                m_nielsen.set_sat_node(m_nielsen.root());
                 return FC_DONE;
             default: 
                 break;
@@ -482,7 +482,7 @@ namespace smt {
     // -----------------------------------------------------------------------
 
     void theory_nseq::init_model(model_generator& mg) {
-        m_model.init(mg, m_nielsen, m_state);
+        m_model.init(mg, m_nielsen);
     }
 
     model_value_proc* theory_nseq::mk_value(enode* n, model_generator& mg) {
@@ -797,18 +797,17 @@ namespace smt {
         // Group membership indices by variable snode id.
         // Only consider memberships whose string snode is a plain variable (s_var).
         u_map<unsigned_vector> var_to_mems;
-        bool all_var_str = true;
+        bool all_primitive = true;
 
         for (unsigned i = 0; i < mems.size(); ++i) {
             auto const& mem = mems[i];
-            if (!mem.m_str || !mem.m_regex)
+            SASSERT(mem.m_str && mem.m_regex);
-                continue;
+            if (mem.is_primitive()) {
-            if (mem.m_str->is_var()) {
                 auto& vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector());
                 vec.push_back(i);
             }
             else
-                all_var_str = false;
+                all_primitive = false;
         }
 
         if (var_to_mems.empty())
@@ -860,7 +859,7 @@ namespace smt {
         // All variables' regex intersections are non-empty.
         // If there are no word equations and no disequalities, variables are
         // independent and each can be assigned a witness string → SAT.
-        if (all_var_str && m_state.str_eqs().empty() && m_state.diseqs().empty() && !has_unhandled_preds()) {
+        if (all_primitive && m_state.str_eqs().empty() && m_state.diseqs().empty() && !has_unhandled_preds()) {
             TRACE(seq, tout << "nseq regex precheck: all intersections non-empty, "
                             << "no word eqs/diseqs → SAT\n";);
             return l_false;  // signals SAT (non-empty / satisfiable)