mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Merge pull request #303 from NikolajBjorner/master

Browse source 
toggle default for bv2int decision procedure support to avoid confusi…
This commit is contained in:
Nikolaj Bjorner 2015-11-10 15:10:43 -05:00
parent 746689904d 315dc80eb0
commit 1ad45783b1
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params_helper.pyg
View file

@ -33,7 +33,7 @@ def_module_params(module_name='smt',
('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, False, 'enable support for int2bv and bv2int operators'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),

2
src/smt/params/theory_bv_params.h
View file

@ -39,7 +39,7 @@ struct theory_bv_params {
m_bv_lazy_le(false),
m_bv_cc(false),
m_bv_blast_max_size(INT_MAX),
m_bv_enable_int2bv2int(false) {
m_bv_enable_int2bv2int(true) {
updt_params(p);
}