diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 3c04bc5a43..9753e42072 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -101,7 +101,7 @@ def_module_params(module_name='smt', ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), - ('arith.nl.propagate_fixed_rows', BOOL, True, 'scan LP rows for fixed variables'), + ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'), ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),