From 339f0cd5f93c8d5c3ee5da7fee4cbe73ab914eb2 Mon Sep 17 00:00:00 2001
From: Ruijie Fang <57693513+ruijiefang@users.noreply.github.com>
Date: Tue, 30 Sep 2025 11:55:14 -0500
Subject: [PATCH] Correctly distinguish between `Lambda` and `Quantifier` in Z3
 Java API (#7955)

* Distinguish between Quantifier and Lambda in AST.java

* Distinguish betwee Lambda and Quantifier in Expr.java

* Make things compile
---
 src/api/java/AST.java    |  8 +++++++-
 src/api/java/Expr.java   | 11 +++++++++--
 src/api/java/Lambda.java |  2 +-
 3 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 99cdde948..0257f5294 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.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), 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:
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 60826665d..910869bcd 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -2148,8 +2148,15 @@ public class Expr<R extends Sort> extends AST
     static Expr<?> create(Context ctx, long obj)
     {
         Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
-        if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
-            return new Quantifier(ctx, 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.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
+            if (isLambda) {
+               return new Lambda(ctx, obj);
+            } else {
+               return new Quantifier(ctx, obj);
+            }
+		}
         long s = Native.getSort(ctx.nCtx(), obj);
         Z3_sort_kind sk = Z3_sort_kind
                 .fromInt(Native.getSortKind(ctx.nCtx(), s));
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<R extends Sort> extends ArrayExpr<Sort, R>
    }
 
 
-    private Lambda(Context ctx, long obj)
+    Lambda(Context ctx, long obj)
     {
         super(ctx, obj);
     }