3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
This commit is contained in:
Nikolaj Bjorner 2016-02-10 12:02:51 +00:00
commit 84cf208d5f

View file

@ -15,7 +15,7 @@ def_module_params(module_name='smt',
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
('timeout', UINT, 0, 'timeout (0 means no timeout)'),
('timeout', UINT, 0, 'timeout (in milliseconds) (0 means no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),