let mk_bool_var ctx name = mk_var ctx name (Z3.mk_bool_sort ctx)