From a5e1e7f5d2d4dc886d49ae686b0f9adccf91317e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jan 2025 19:10:25 -0800 Subject: [PATCH] set lookahead mode to default Signed-off-by: Nikolaj Bjorner --- src/params/sls_params.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg index ce1d760d1..1ec140c95 100644 --- a/src/params/sls_params.pyg +++ b/src/params/sls_params.pyg @@ -25,7 +25,7 @@ def_module_params('sls', ('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'), ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), ('random_seed', UINT, 0, 'random seed'), - ('arith_use_lookahead', BOOL, False, 'use lookahead solver for NIRA'), + ('arith_use_lookahead', BOOL, True, 'use lookahead solver for NIRA'), ('arith_allow_plateau', BOOL, False, 'allow plateau moves during NIRA solving'), ('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'), ('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),