From 3147d2351d50a4eca7d97b380f86038ef31e98da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Aug 2019 08:06:38 -0700 Subject: [PATCH] fix #2460 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Quantifier.cs | 4 ++-- src/api/java/Quantifier.java | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index 57d38e7c1..f531c97f1 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -143,12 +143,12 @@ namespace Microsoft.Z3 /// /// The body of the quantifier. /// - public BoolExpr Body + public Expr Body { get { - return (BoolExpr)Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); + return Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); } } diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 73b726e8d..6b2f1d4fc 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -139,9 +139,9 @@ public class Quantifier extends BoolExpr * * @throws Z3Exception **/ - public BoolExpr getBody() + public Expr getBody() { - return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext() + return Expr.create(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); }