From c980cfd783fd9ff297e7971b695a2e425b6f7d60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Jun 2017 20:51:55 -0700
Subject: [PATCH] add concat recognizer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/java/Expr.java | 9 +++++++++
 1 file changed, 9 insertions(+)

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