Update documentation for using docker, run a CI test for the docker i…

…mages, and add a newer z3 package into the Ubuntu docker image (installed via opam)

.github/workflows/docker.yml

@@ -82,3 +82,16 @@ jobs:
         attests: type=sbom
         provenance: mode=max
         github-token: ${{ secrets.GITHUB_TOKEN }}
+
+  test-docker-images:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        tag: [release, release-redhat]
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Run CN CI tests
+      run: |
+        docker pull ${{env.CERBERUS_IMAGE_ID}}:${{ matrix.tag }}
+        docker run -v $PWD:/work ${{env.CERBERUS_IMAGE_ID}}:${{ matrix.tag }} tests/run-cn.sh

Dockerfile.ubuntu

@@ -11,6 +11,7 @@ RUN opam init --disable-sandboxing
 ADD . /opt/cerberus
 WORKDIR /opt/cerberus
 RUN opam install --deps-only  ./cerberus-lib.opam ./cn.opam
+RUN opam install z3
 
 RUN eval `opam env` \
   && make install_cn

README.md

@@ -183,10 +183,22 @@ See https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md
 Docker image
 ------------
 
+A pre-build docker image with `cerberus` and `cn` can be downloaded with:
+
+* For the Ubuntu 22.04 based image (recommended):
+    ```bash
+    $ docker pull ghcr.io/rems-project/cerberus/cn:release
+    ```
+* For Redhat Ubi9 based image:
+    ```bash
+    $ docker pull ghcr.io/rems-project/cerberus/cn:release-redhat
+    ```
+
+For a local build, run:
 ```bash
-$ make -f Makefile_docker
+$ docker build -t cn:release -f Dockerfile.ubuntu .
 ```
-creates a Docker image than can be used for example with:
+which creates a Docker image than can be used for example with:
 ```bash
 $ docker run --volume `PWD`:/data/ cerberus:0.1 tests/tcc/00_assignment.c --pp=core
 ```

backend/cn/README.md

@@ -18,7 +18,7 @@ and their dependencies.
    Note: there is a [known bug with Z3 version
    4.8.13](https://github.com/rems-project/cerberus/issues/663) (the default on
    Ubuntu 22.04) so you may wish to install Z3 via opam later for a more
-   up-to-date version. CVC5 
+   up-to-date version. Z3 that is provided in the docker images is sufficiently up-to-date.
 
 2. Install the opam package manager for OCaml:
    https://ocaml.org/docs/installing-ocaml#install-opam.