mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

ml build failure, issue #403

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-07 20:14:43 -08:00
parent 17a32a4e5f
commit 183d3821ce
1 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/api/ml/z3.ml
View file

@ -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))