From d2a3b53d927c8f0d0523b747f2b6d69c99c98695 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Feb 2019 12:28:17 -0800 Subject: [PATCH] fix remaining incorrect uses of new BoolExpr related to #2125 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Goal.cs | 2 +- src/api/dotnet/Lambda.cs | 2 +- src/api/dotnet/Quantifier.cs | 2 +- src/api/java/Lambda.java | 4 ++-- src/api/java/Quantifier.java | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 4dbc78b7e..883b91f35 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -144,7 +144,7 @@ namespace Microsoft.Z3 uint n = Size; BoolExpr[] res = new BoolExpr[n]; for (uint i = 0; i < n; i++) - res[i] = new BoolExpr(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i)); + res[i] = (BoolExpr)Expr.Create(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i)); return res; } } diff --git a/src/api/dotnet/Lambda.cs b/src/api/dotnet/Lambda.cs index 35497f88f..1cd9db2dd 100644 --- a/src/api/dotnet/Lambda.cs +++ b/src/api/dotnet/Lambda.cs @@ -76,7 +76,7 @@ namespace Microsoft.Z3 get { - return new BoolExpr(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/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index f4a889092..57d38e7c1 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -148,7 +148,7 @@ namespace Microsoft.Z3 get { - return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); + return (BoolExpr)Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); } } diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java index 45375fb29..cf9809a23 100644 --- a/src/api/java/Lambda.java +++ b/src/api/java/Lambda.java @@ -70,9 +70,9 @@ import com.microsoft.z3.enumerations.Z3_ast_kind; * * @throws Z3Exception **/ - public BoolExpr getBody() + public Expr getBody() { - return new BoolExpr(getContext(), Native.getQuantifierBody(getContext() + return Expr.create(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); } diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 29483d1aa..73b726e8d 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -141,7 +141,7 @@ public class Quantifier extends BoolExpr **/ public BoolExpr getBody() { - return new BoolExpr(getContext(), Native.getQuantifierBody(getContext() + return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); }