From fa97f4a62620f8758d74c5d678e674d4e5ae3d41 Mon Sep 17 00:00:00 2001 From: Nicola Mometto Date: Tue, 26 Mar 2019 14:16:31 +0000 Subject: [PATCH] fix name clash in ocaml api --- src/api/ml/z3.ml | 2 +- src/api/ml/z3.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 5fb87bf64..50735a57c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -717,7 +717,7 @@ struct else mk_exists ctx sorts names body weight patterns nopatterns quantifier_id skolem_id - let mk_quantifier (ctx:context) (universal:bool) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = + let mk_quantifier_const (ctx:context) (universal:bool) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = if universal then mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id else diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 4b6d8bc25..f93769731 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -746,7 +746,7 @@ sig val mk_quantifier : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier (** Create a Quantifier. *) - val mk_quantifier : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier + val mk_quantifier_const : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier (** A string representation of the quantifier. *) val to_string : quantifier -> string