let mk_int_var ctx name = mk_var ctx name (Z3.mk_int_sort ctx)