mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge pull request #444 from delcypher/explicit_solver_timeout_units

Browse source 
Explicitly state what the units of the timeout parameter for the "smt" module are.
This commit is contained in:
Nikolaj Bjorner 2016-02-10 11:43:31 +00:00
parent 5285a795ac ea900db337
commit 56f15e98b5
1 changed files with 1 additions and 1 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

@ -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)'),