From 8ac7a242eb93f95175c5d82ad346f40048c594ba Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 5 Jun 2026 19:19:08 +0200 Subject: [PATCH] Z3 arguments got ignored in the Nielsen graph --- src/smt/seq/seq_nielsen.h | 12 ++++++------ src/smt/theory_nseq.cpp | 22 ++++++++++------------ 2 files changed, 16 insertions(+), 18 deletions(-) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index eb08c110f..dd24d21a0 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -1074,18 +1074,18 @@ namespace seq { unsigned num_nodes() const { return m_nodes.size(); } // maximum overall search depth (0 = unlimited) - void set_max_search_depth(unsigned d) { m_max_search_depth = d; } + void set_max_search_depth(const unsigned d) { m_max_search_depth = d; } // maximum total DFS nodes per solve() call (0 = unlimited) - void set_max_nodes(unsigned n) { m_max_nodes = n; } + void set_max_nodes(const unsigned n) { m_max_nodes = n; } // enable/disable Parikh image verification constraints - void set_parikh_enabled(bool e) { m_parikh_enabled = e; } + void set_parikh_enabled(const bool e) { m_parikh_enabled = e; } - void set_signature_split(bool e) { m_signature_split = e; } + void set_signature_split(const bool e) { m_signature_split = e; } - void set_regex_factorization_threshold(unsigned max) { m_regex_factorization_threshold = max; } - void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; } + void set_regex_factorization_threshold(const unsigned max) { m_regex_factorization_threshold = max; } + void set_regex_factorization_eager(const bool e) { m_regex_factorization_eager = e; } // display for debugging std::ostream& display(std::ostream& out) const; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index b7dd8ef48..06bc02bd0 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -829,26 +829,24 @@ namespace smt { // let's rebuild the whole Nielsen graph populate_nielsen_graph(); - // assert length constraints derived from string equalities - if (assert_length_constraints()) { - TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n"); - return FC_CONTINUE; - } - - SASSERT(m_nielsen.root()); - - m_nielsen.assert_node_side_constraints(m_nielsen.root()); - - ++m_num_final_checks; - m_nielsen.set_max_search_depth(get_fparams().m_nseq_max_depth); m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes); m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); m_nielsen.set_signature_split(get_fparams().m_nseq_signature); m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold); m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager); + + // assert length constraints derived from string equalities + if (assert_length_constraints()) { + TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n"); + return FC_CONTINUE; + } + SASSERT(m_nielsen.root()); + m_nielsen.assert_node_side_constraints(m_nielsen.root()); } + ++m_num_final_checks; + SASSERT(!m_nielsen.root()->is_currently_conflict()); // Regex membership pre-check: before running DFS, check intersection