diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 20986e438..9dc53133e 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -835,15 +835,14 @@ end = struct let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in expr_of_ptr ctx o - let apply1 ctx f t = - expr_of_ptr ctx (f (context_gno ctx) (gno t)) + let apply1 ctx f t = + expr_of_ptr ctx (f (context_gno ctx) (gno t)) - let apply2 ctx f t1 t2 = - expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) - - let apply3 ctx f t1 t2 t3 = - expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) + let apply2 ctx f t1 t2 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) + let apply3 ctx f t1 t2 t3 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) let simplify ( x : expr ) ( p : Params.params option ) = match p with | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x))