let
mk_real_var ctx name = mk_var ctx name (
Z3
.mk_real_sort ctx)