mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-20 00:49:33 +00:00
Code Activity

Fixed regex factorization again

Browse source
This commit is contained in:
CEisenhofer 2026-05-04 19:25:07 +02:00
parent adb9ca4305
commit 5b3d734ecb
6 changed files with 28 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_nseq.cpp
View file

@ -468,7 +468,7 @@ namespace smt {
if (s_expr)
ensure_length_var(s_expr);
if (!get_fparams().m_nseq_regex_factorization)
if (!get_fparams().m_nseq_regex_factorization_threshold)
return;
// Boolean Closure Propagations
@ -709,7 +709,7 @@ namespace smt {
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(get_fparams().m_nseq_regex_factorization);
m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
SASSERT(!m_nielsen.root()->is_currently_conflict());