diff --git a/src/tactic/smtlogics/qfbv_tactic_params.pyg b/src/tactic/smtlogics/qfbv_tactic_params.pyg
new file mode 100644
index 000000000..8dccfc650
--- /dev/null
+++ b/src/tactic/smtlogics/qfbv_tactic_params.pyg
@@ -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")
+                  ))