z3-src 415.4.4

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation
1
2
3
4
5
6
7
8
def_module_params(module_name='rewriter',
                  class_name='ackermannize_bv_tactic_params',
                  export=True,
                  params=(
                          ("div0_ackermann_limit", UINT, 1000, "a bound for number of congruence Ackermann lemmas for div0 modelling"),
                          )
                  )