mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

ml build failure

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

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

@ -835,11 +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)) in
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)) in
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)) in
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