mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Adding parameters to Ackermannization in qfbv_tactic.

Browse source
This commit is contained in:
mikolas 2016-01-29 17:21:21 +00:00
parent c9799b143d
commit de28e57dee
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/smtlogics/qfbv_tactic_params.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params(class_name='qfbv_tactic_params',
module_name="smtlogic_tactic",
export=True,
params=(('div0ackermann', BOOL, False, "if true, then try to Ackermannize div etc functions."),
("div0_ackermann_limit", UINT, 1000, "a bound for number of congregants Ackerman lemmas")
))