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..69dbfa23d 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -743,10 +743,10 @@ sig val mk_lambda : context -> (Symbol.symbol * Sort.sort) list -> Expr.expr -> quantifier (** Create a Quantifier. *) - 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 + val mk_quantifier : context -> bool -> 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