mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Explicitly state what the units of the timeout parameter for the "smt"

Browse source 
module are.
This commit is contained in:
Dan Liew 2016-02-10 11:35:15 +00:00
parent 4ba744987d
commit ea900db337
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params_helper.pyg
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)'),