From 121f66c19ce0dbe131b64db2f6d03ab827cecb3e Mon Sep 17 00:00:00 2001
From: Ruijie Fang <57693513+ruijiefang@users.noreply.github.com>
Date: Mon, 29 Sep 2025 21:47:11 -0500
Subject: [PATCH] Distinguish between Quantifier and Lambda in AST.java

---
 src/api/java/AST.java | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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<AST>
         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: