diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 71a2e3e1e..707f3300d 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1297,6 +1297,15 @@ public class Expr extends AST return Native.getString(getContext().nCtx(), getNativeObject()); } + /** + * Check whether expression is a concatenation + * @return a boolean + */ + public boolean isConcat() + { + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT; + } + /** * Indicates whether the term is a binary equivalence modulo namings. * Remarks: This binary predicate is used in proof terms. It captures