Update Dockerfiles to bump standard Z3 version to 4.8.11

Dockerfile

@@ -25,9 +25,17 @@ RUN    apt-get update        \
         pkg-config           \
         python3              \
         python3-graphviz     \
-        z3                   \
         zlib1g-dev
 
+RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.11 \
+    && cd z3                                                         \
+    && python scripts/mk_make.py                                     \
+    && cd build                                                      \
+    && make -j8                                                      \
+    && make install                                                  \
+    && cd ../..                                                      \
+    && rm -rf z3
+
 RUN curl -sL https://deb.nodesource.com/setup_14.x | bash -
 RUN    apt-get update               \
     && apt-get upgrade --yes        \

README.md

@@ -100,8 +100,11 @@ The following dependencies are needed either at build time or runtime:
 *   [python](https://www.python.org)
 *   [stack](https://docs.haskellstack.org/en/stable/README/)
 *   [zlib](https://www.zlib.net/)
-*   [z3](https://github.com/Z3Prover/z3) (on some distributions libz3 is also needed and packaged separately)
-    Note that you need at least version 4.6 of Z3, and we recommend at least version 4.8.
+*   [z3](https://github.com/Z3Prover/z3) (on some distributions libz3 is also
+    needed and packaged separately) Note that you need version 4.8.11 of Z3,
+    which may require you to build and install from source if your package
+    manager does not supply it. Other versions are known to have bugs and
+    performance regressions likely to cause issues in the K test suite.
 
 The following dependencies are optional and are only needed when building
 the OCaml backend (**not recommended**):

k-distribution/INSTALL.md

@@ -54,6 +54,13 @@ Pre-installation Notes
     [instructions below](#installing-the-ocaml-backend-optional) on using the
     OCaml backend with the package-installed K.
 
+-   K depends on version 4.8.11 of Z3, which may not be supplied by package
+    managers. If this is the case, it should be built and installed from source
+    following the
+    [instructions](https://github.com/Z3Prover/z3#building-z3-using-cmake) in
+    the Z3 repository. Other versions (older and newer) are not supported by K,
+    and may lead to incorrect behaviour or performance issues.
+
 Downloading Packages
 --------------------
 

k-distribution/include/kframework/builtin/domains.md

@@ -909,6 +909,10 @@ You can:
 
 * Compute the bitwise complement `~Int` of an integer value in twos-complement.
 * Compute the exponentiation `^Int` of two integers.
+  * As implemented above, the frontend will only send integer exponentiation to
+    Z3 if both the base and exponent are positive integers. This prevents the K
+    frontend from running afoul of the potentially undefined or inconsistent Z3
+    behaviour in cases where `#1` or `#2` are non-positive.
 * Compute the exponentiation of two integers modulo another integer (`^%Int`).
   `A ^%Int B C` is equal in value to `(A ^Int B) %Int C`, but has a better
   asymptotic complexity.
@@ -930,7 +934,7 @@ You can:
 ```k
   syntax Int ::= "~Int" Int                     [function, klabel(~Int_), symbol, functional, latex(\mathop{\sim_{\scriptstyle\it Int}}{#1}), hook(INT.not), smtlib(notInt)]
                > left:
-                 Int "^Int" Int                 [function, klabel(_^Int_), symbol, left, smt-hook(^), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)]
+                 Int "^Int" Int                 [function, klabel(_^Int_), symbol, left, smt-hook((ite (and (< 0 #1) (< 0 #2)) 0 (to_int (^ #1 #2)))), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)]
                | Int "^%Int" Int Int            [function, klabel(_^%Int__), symbol, left, smt-hook((mod (^ #1 #2) #3)), hook(INT.powmod)]
                > left:
                  Int "*Int" Int                 [function, functional, klabel(_*Int_), symbol, left, smt-hook(*), latex({#1}\mathrel{\ast_{\scriptstyle\it Int}}{#2}), hook(INT.mul)]
@@ -1055,6 +1059,14 @@ module INT-SYMBOLIC [symbolic]
   rule X modInt N => X requires 0 <=Int X andBool X <Int N [simplification]
   rule X   %Int N => X requires 0 <=Int X andBool X <Int N [simplification]
 
+  rule  1 ^Int _ =>  1                            [simplification]
+  rule -1 ^Int N =>  1 requires N %Int 2 ==Int  0 [simplification]
+  rule -1 ^Int N => -1 requires N %Int 2 =/=Int 0 [simplification]
+  rule  0 ^Int N =>  0 requires N >Int 0          [simplification]
+  rule  X ^Int N =>  0 requires absInt(X) >Int 1
+                        andBool N <Int 0          [simplification]
+  rule  X ^Int 0 =>  1 requires X =/=Int 0        [simplification]
+
   // Bit-shifts
   rule X <<Int 0 => X [simplification]
   rule 0 <<Int _ => 0 [simplification]

k-distribution/tests/regression-new/issue-2154-smt-power/Makefile

@@ -0,0 +1,9 @@
+DEF=test
+EXT=test
+KOMPILE_FLAGS=--syntax-module TEST
+KOMPILE_BACKEND?=haskell
+KPROVE_FLAGS=
+
+TESTDIR=.
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/issue-2154-smt-power/test-spec.k

@@ -0,0 +1,9 @@
+require "test.k"
+
+module TEST-SPEC
+    imports TEST
+
+    claim <k> runLemma(3 ^Int X <=Int 3 ^Int Y) => doneLemma(true) ... </k>
+      requires 0 <Int X andBool 0 <Int Y
+       andBool X <=Int Y
+endmodule

k-distribution/tests/regression-new/issue-2154-smt-power/test-spec.k.out

@@ -0,0 +1 @@
+#Top

k-distribution/tests/regression-new/issue-2154-smt-power/test.k

@@ -0,0 +1,17 @@
+requires "domains.md"
+
+module TEST
+    imports BOOL
+    imports INT-SYMBOLIC
+
+    syntax KItem ::= runLemma ( Bool ) | doneLemma ( Bool )
+ // -------------------------------------------------------
+    rule <k> runLemma(B) => doneLemma(B) ... </k>
+
+    rule N ^Int N' <=Int M ^Int M' => true
+      requires 0 <Int N andBool 0 <Int N'
+       andBool 0 <Int M andBool 0 <Int M'
+       andBool N <=Int M andBool N' <=Int M'
+      [simplification, smt-lemma]
+
+endmodule

package/debian/Dockerfile

@@ -33,11 +33,19 @@ RUN    apt-get update            \
         pkg-config               \
         python3                  \
         python3-graphviz         \
-        z3                       \
         zlib1g-dev
 
 RUN curl -sSL https://get.haskellstack.org/ | sh
 
+RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.11 \
+    && cd z3                                                         \
+    && python scripts/mk_make.py                                     \
+    && cd build                                                      \
+    && make -j8                                                      \
+    && make install                                                  \
+    && cd ../..                                                      \
+    && rm -rf z3
+
 ARG USER_ID=1000
 ARG GROUP_ID=1000
 RUN    groupadd -g $GROUP_ID user                     \

package/docker/Dockerfile.ubuntu-bionic

@@ -10,13 +10,13 @@ RUN    apt-get update                   \
                         git             \
                         python
 
-RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.6 \
-    && cd z3                                                        \
-    && python scripts/mk_make.py                                    \
-    && cd build                                                     \
-    && make -j8                                                     \
-    && make install                                                 \
-    && cd ../..                                                     \
+RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.11 \
+    && cd z3                                                         \
+    && python scripts/mk_make.py                                     \
+    && cd build                                                      \
+    && make -j8                                                      \
+    && make install                                                  \
+    && cd ../..                                                      \
     && rm -rf z3
 
 COPY kframework_amd64_bionic.deb /kframework_amd64_bionic.deb

package/docker/Dockerfile.ubuntu-focal

@@ -10,13 +10,13 @@ RUN    apt-get update                   \
                         git             \
                         python
 
-RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.6 \
-    && cd z3                                                        \
-    && python scripts/mk_make.py                                    \
-    && cd build                                                     \
-    && make -j8                                                     \
-    && make install                                                 \
-    && cd ../..                                                     \
+RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.11 \
+    && cd z3                                                         \
+    && python scripts/mk_make.py                                     \
+    && cd build                                                      \
+    && make -j8                                                      \
+    && make install                                                  \
+    && cd ../..                                                      \
     && rm -rf z3
 
 COPY kframework_amd64_focal.deb /kframework_amd64_focal.deb