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; } /**