From d86c049df25df9b8ca37cc67d245c9da9e929dc7 Mon Sep 17 00:00:00 2001 From: Ruijie Fang Date: Mon, 29 Sep 2025 21:52:54 -0500 Subject: [PATCH] Make things compile --- src/api/java/AST.java | 2 +- src/api/java/Expr.java | 2 +- src/api/java/Lambda.java | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index c2e4208c9..0257f5294 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -209,7 +209,7 @@ public class AST extends Z3Object implements Comparable return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: // a quantifier AST is a lambda iff it is neither a forall nor an exists. - boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj); + boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); if (isLambda) { return new Lambda(ctx, obj); } else { diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 96e2e2c38..910869bcd 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2150,7 +2150,7 @@ public class Expr extends AST Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) { // a quantifier AST is a lambda iff it is neither a forall nor an exists. - boolean isLambda = !Native.isQuantifierExists(ctx, obj) && !Native.isQuantifierForall(ctx, obj); + boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj); if (isLambda) { return new Lambda(ctx, obj); } else { diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java index 780e543c8..a42dfbf45 100644 --- a/src/api/java/Lambda.java +++ b/src/api/java/Lambda.java @@ -126,7 +126,7 @@ public class Lambda extends ArrayExpr } - private Lambda(Context ctx, long obj) + Lambda(Context ctx, long obj) { super(ctx, obj); }