Give Z3 smt label to integer and operation to support ABI verification.

kframework · Nov 15, 2017 · 1b4fb8e · 1b4fb8e
1 parent 3debc40
commit 1b4fb8e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 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
@@ -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
@@ -311,7 +311,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: