let
mk_var ctx name ty =
Z3
.mk_const ctx (
Z3
.mk_string_symbol ctx name) ty