From 939ba4392ac2b6886bbe5afedf455a9788bb1004 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Aug 2026 12:59:36 -0700 Subject: [PATCH] Enable monadic regex solver by default (#10466) ## Summary - set \smt.seq.regex_monadic\ to \ rue\ by default - keep the existing option available for explicitly disabling the monadic regex solver ## Testing - regenerated and built the parameter helpers and Z3 shell - confirmed \z3 -p\ reports \seq.regex_monadic (default: true)\`n- ran the complete unit test suite Copilot-Session: 2b211510-693f-4df8-9ebb-3db1e08f8683 --- src/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 643b5e9e26..abe244ebd2 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -142,7 +142,7 @@ def_module_params(module_name='smt', ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'), ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), - ('seq.regex_monadic', BOOL, False, 'use the monadic regular-expression end-game solver'), + ('seq.regex_monadic', BOOL, True, 'use the monadic regular-expression end-game solver'), ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'), ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),