3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00

change default to _not_ include auxiliary functions in model as this seems to break fewer'

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-23 09:51:06 -07:00
parent d790523c59
commit 365b8f3281

View file

@ -5,7 +5,7 @@ def_module_params('model',
('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'), ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
('compact', BOOL, True, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), ('compact', BOOL, True, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'), ('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'),
('user_functions', BOOL, True, 'include user defined functions in model'), ('user_functions', BOOL, False, 'include user defined functions in model'),
('completion', BOOL, False, 'enable/disable model completion'), ('completion', BOOL, False, 'enable/disable model completion'),
)) ))