From 887ecc0c98345533ab1ba28003d4e79fefd351c5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 22 Oct 2025 21:36:22 -0700 Subject: [PATCH] throttle grobner method more actively Signed-off-by: Lev Nachmanson --- 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 e0d02c6d2..451a07964 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -80,7 +80,7 @@ def_module_params(module_name='smt', ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'), ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'), - ('arith.nl.grobner_exp_delay', BOOL, False, 'use exponential delay between grobner basis attempts'), + ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),