Skip to content

Commit 3147d23

Browse files
fix #2460
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent 4431a53 commit 3147d23

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

src/api/dotnet/Quantifier.cs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -143,12 +143,12 @@ public Sort[] BoundVariableSorts
143143
/// <summary>
144144
/// The body of the quantifier.
145145
/// </summary>
146-
public BoolExpr Body
146+
public Expr Body
147147
{
148148
get
149149
{
150150

151-
return (BoolExpr)Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
151+
return Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
152152
}
153153
}
154154

src/api/java/Quantifier.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -139,9 +139,9 @@ public Sort[] getBoundVariableSorts()
139139
*
140140
* @throws Z3Exception
141141
**/
142-
public BoolExpr getBody()
142+
public Expr getBody()
143143
{
144-
return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext()
144+
return Expr.create(getContext(), Native.getQuantifierBody(getContext()
145145
.nCtx(), getNativeObject()));
146146
}
147147

0 commit comments

Comments
 (0)