From dd127c2f7194caed03096853050526fb141eeeeb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Jan 2013 18:16:29 +0000 Subject: [PATCH] Java API: bugfix Signed-off-by: Christoph M. Wintersteiger --- src/api/java/AST.java | 8 ++++++++ src/api/java/Expr.java | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index b7d048a1e..60ff48ecb 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -138,6 +138,14 @@ public class AST extends Z3Object } } + /** + * Indicates whether the AST is an application + **/ + public boolean IsApp() throws Z3Exception + { + return this.ASTKind() == Z3_ast_kind.Z3_APP_AST; + } + /** * Indicates whether the AST is a BoundVariable **/ diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index a67d94e7e..09456307f 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -204,7 +204,7 @@ public class Expr extends AST **/ public boolean IsConst() throws Z3Exception { - return IsExpr() && NumArgs() == 0 && FuncDecl().DomainSize() == 0; + return IsApp() && NumArgs() == 0 && FuncDecl().DomainSize() == 0; } /**