mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

spacer: switch to new IUC as default

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-30 09:11:16 -07:00
parent 3a97451f8c
commit fb52c36210
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/base/fixedpoint_params.pyg
View file

@ -181,11 +181,11 @@ def_module_params('fixedpoint',
('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
('spacer.q3.instantiate', BOOL, True, 'instantiate quantified lemmas'), ('spacer.q3.instantiate', BOOL, True, 'instantiate quantified lemmas'),
('spacer.q3', BOOL, True, 'allow quantified lemmas in frames'), ('spacer.q3', BOOL, True, 'allow quantified lemmas in frames'),
('spacer.iuc', UINT, 0, ('spacer.iuc', UINT, 1,
'0 = use old implementation of unsat-core-generation, ' + '0 = use old implementation of unsat-core-generation, ' +
'1 = use new implementation of IUC generation, ' + '1 = use new implementation of IUC generation, ' +
'2 = use new implementation of IUC + min-cut optimization'), '2 = use new implementation of IUC + min-cut optimization'),
('spacer.iuc.arith', UINT, 0, ('spacer.iuc.arith', UINT, 1,
'0 = use simple Farkas plugin, ' + '0 = use simple Farkas plugin, ' +
'1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),' + '1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),' +
'2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'), '2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'),