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.'),