diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 99cdde948..c2e4208c9 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable case Z3_FUNC_DECL_AST: return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: - return new Quantifier(ctx, obj); + // 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); + if (isLambda) { + return new Lambda(ctx, obj); + } else { + return new Quantifier(ctx, obj); + } case Z3_SORT_AST: return Sort.create(ctx, obj); case Z3_APP_AST: