let
mk_int ctx v =
Z3
.mk_int ctx v (
Z3
.mk_int_sort ctx)