mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
ensure arith.reflect has default true
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3f89c1418b
commit
6f2cd4817b
|
@ -44,7 +44,7 @@ def_module_params(module_name='smt',
|
|||
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
|
||||
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
|
||||
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
|
||||
('arith.reflect', BOOL, False, 'reflect arithmetical operators to the congruence closure'),
|
||||
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),
|
||||
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
|
||||
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
|
||||
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
|
||||
|
|
Loading…
Reference in a new issue