From 77a83f5f4b238d54383c3727be2075bc320170b2 Mon Sep 17 00:00:00 2001
From: Brandon Moore <brandon.moore@runtimeverification.com>
Date: Fri, 29 Sep 2017 15:44:42 -0500
Subject: [PATCH] Give Z3 smt label to integer and operation to support ABI
 verification.

---
 .../java/org/kframework/backend/java/symbolic/KILtoSMTLib.java  | 1 +
 k-distribution/include/builtin/domains.k                        | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java
index 7ce66cb00c..4e6b40deb7 100644
--- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java
+++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java
@@ -85,6 +85,7 @@ public class KILtoSMTLib extends CopyOnWriteTransformer {
             "int_max",
             "int_min",
             "int_abs",
+            "int_and",
             /* extra float theory */
             "remainder",
             "min",
diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k
index 67fe96eb8f..d573a3339b 100644
--- a/k-distribution/include/builtin/domains.k
+++ b/k-distribution/include/builtin/domains.k
@@ -312,7 +312,7 @@ module INT
                  Int ">>Int" Int                [function, left, latex({#1}\mathrel{\gg_{\scriptstyle\it Int}}{#2}), hook(INT.shr)]
                | Int "<<Int" Int                [function, left, latex({#1}\mathrel{\ll_{\scriptstyle\it Int}}{#2}), hook(INT.shl)]
                > left:
-                 Int "&Int" Int                 [function, left, latex({#1}\mathrel{\&_{\scriptstyle\it Int}}{#2}), hook(INT.and)]
+                 Int "&Int" Int                 [function, left, smtlib(int_and), latex({#1}\mathrel{\&_{\scriptstyle\it Int}}{#2}), hook(INT.and)]
                > left:
                  Int "xorInt" Int               [function, left, latex({#1}\mathrel{\oplus_{\scriptstyle\it Int}}{#2}), hook(INT.xor)]
                > left: