mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add arguments to optimize_check fix #1866

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-14 20:43:35 -07:00
parent 0457b5a73f
commit 09e40f6e23
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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