From 09e40f6e23351c3da40676b81c61b5f7ee82b234 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Oct 2018 20:43:35 -0700 Subject: [PATCH] add arguments to optimize_check fix #1866 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 3c583eaef..d1049615c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -707,7 +707,8 @@ struct let mk_exists_const = _internal_mk_quantifier_const ~universal:false let mk_lambda_const ctx bound body = Z3native.mk_lambda_const ctx (List.length bound) bound body let mk_lambda ctx bound body = - let (names, sorts) = List.unzip bound in + let names = List.map (fun (x,_) -> x) bound in + let sorts = List.map (fun (_,y) -> y) bound in Z3native.mk_lambda ctx (List.length bound) sorts names body let mk_quantifier (ctx:context) (universal:bool) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =