mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
set lookahead mode to default
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
158dea575b
commit
a5e1e7f5d2
|
@ -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'),
|
||||
|
|
Loading…
Reference in a new issue