let
mk_binary_app ctx f x y =
Z3
.mk_app ctx f [|x;y|]