diff --git a/docker/Dockerfile b/docker/Dockerfile
deleted file mode 100644
index 9caefb8aee83c799ff58189eb89214dd6e5000c8..0000000000000000000000000000000000000000
--- a/docker/Dockerfile
+++ /dev/null
@@ -1,21 +0,0 @@
-FROM ocaml/opam:debian-10-ocaml-4.11
-
-RUN sudo apt-get update &&\
-    sudo apt-get install -y cvc4 z3
-
-RUN opam repository set-url default "https://opam.ocaml.org" &&\
-    opam repository add lustrec "https://gitlab.isae-supaero.fr/lustrec/opam-repository.git" &&\
-    opam update &&\
-    opam depext -i\
-    dune.2.9.1 dune-site menhir zarith ppx_deriving_yojson ocamlgraph alt-ergo frama-c.24.0 re
-ENV PATH=$PATH:/home/opam/.opam/4.11/bin
-
-RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
-ENV PATH=$PATH:/home/opam/.cargo/bin
-RUN cargo install tokei
-
-RUN why3 config detect
-
-COPY init.sh $HOME/
-
-CMD ["/bin/bash", "--init-file", "~/init.sh"]
diff --git a/docker/Dockerfile-run b/docker/Dockerfile-run
new file mode 100644
index 0000000000000000000000000000000000000000..fa0591e53619349c759830ad68d0315c486ec9e9
--- /dev/null
+++ b/docker/Dockerfile-run
@@ -0,0 +1,48 @@
+# This Dockerfile builds a Debian testing docker image with OCaml
+# 4.11, Frama-C 26.1, Z3 4.11.2 installed through Opam and CVC4 1.8
+# installed as an external binary.
+#
+# It could be run "over" a clone of LustreC repository to test
+# it. Notice that you have to install the LustreC Frama-C
+# lustrec_wp_plugin in order to be able to prove ACSL specifications.
+
+# use Debian image with OCaml and opam installed
+FROM ocaml/opam:debian-testing-ocaml-4.14
+
+# update repository
+RUN sudo apt update
+
+# upgrade opam
+RUN sudo apt install -y opam
+
+# install CVC4 and Z3 from Debian repository
+RUN sudo apt install -y cvc4
+
+# install tokei
+RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
+ENV PATH=$PATH:/home/opam/.cargo/bin
+RUN cargo install tokei
+
+# update local opam repository
+RUN opam repository set-url default "https://opam.ocaml.org" && \
+    opam update
+
+# install Frama-C and Z3
+RUN opam install frama-c.26.1 z3
+
+# set shell and PATH for opam
+SHELL ["/bin/bash", "-c"]
+ENV PATH=$PATH:/home/opam/.opam/4.14/bin
+
+# config Why3 solvers
+RUN why3 config detect
+
+# add init shell script
+ADD init.sh /home/opam/
+
+# start
+CMD /bin/bash --init-file /home/opam/init.sh
+
+# Local Variables:
+# mode: Dockerfile
+# End:
diff --git a/docker/README.md b/docker/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..47c98117300342ec79d5bde23dee8800434db739
--- /dev/null
+++ b/docker/README.md
@@ -0,0 +1,15 @@
+You will find here Dockerfiles needed to build Docker images for
+LustreC.
+
+* `Dockerfile-run`
+
+`Dockerfile-run` builds a Docker image composed of:
+
+- a Debian testing distribution with OCaml 4.14 and CVC4 installed
+- an opam distribution with Frama-C and Z3 installed
+
+This can be used to test LustreC: clone the LustreC repository, pull
+the image and run the `run_docker.sh` script available in the
+`scripts` directory. LustreC and the associated WP strategies are
+built in the host clone of LustreC and you can run tests inside the
+container.
diff --git a/docker/init.sh b/docker/init.sh
index 20f1894f51249e55c111a2e8d53ffd561f8aa3d0..da8f9e31159da3dfa555ff69dd64ce3dcc4124cd 100644
--- a/docker/init.sh
+++ b/docker/init.sh
@@ -1,8 +1,20 @@
-#!/usr/bin/env bash
+# init commands when starting LustreC "run" docker
 
-cd $HOME/lustrec
+# echo PATH
+echo "PATH:" $PATH
 
-echo "Compiling LustreC..."
+# compile LustreC
+cd lustrec
+echo "compiling LustreC..."
 dune clean
 dune build @install
-echo "Done."
+echo "... done!"
+
+# compile LustreC strategies
+cd lustrec_wp_strategies
+echo "installing LustreC WP strategies..."
+opam install .
+echo "... done!"
+
+# get ready
+cd /home/opam/lustrec
diff --git a/scripts/rundocker.sh b/scripts/rundocker.sh
index 361e87e20f4359040abf4b0d2dd70e90277f53e5..7a92ec9045712f39064db91bb609d8adef02ec50 100644
--- a/scripts/rundocker.sh
+++ b/scripts/rundocker.sh
@@ -14,9 +14,15 @@ usage () {
 }
 
 # default values
-CONTAINER_ID=leliobrun/lustrec-env
+CONTAINER_ID=gitlab-registry.isae-supaero.fr/lustrec/lustrec/lustrec-run:latest
 TMP_DIR=/tmp
 
+# check if docker is available
+command -v docker >/dev/null 2>&1 || { \
+        echo >&2 "docker is required but could not be found.  Aborting."; \
+        echo >&2 "To setup Docker: https://docs.docker.com/engine/getstarted/step_one/"; \
+        exit 1; }
+
 # use getopt to get arguments
 TEMP=$(getopt -o 'hi:t:' --long 'help,id:,tmp:' -n 'rundocker.sh' -- "$@")
 
@@ -46,14 +52,8 @@ while true; do
     esac
 done
 
-# check if docker is available
-command -v docker >/dev/null 2>&1 || { \
-        echo >&2 "docker is required but could not be found.  Aborting."; \
-        echo >&2 "To setup Docker: https://docs.docker.com/engine/getstarted/step_one/"; \
-        exit 1; }
-
 # launch docker
-docker run -it --rm --user $(id -u):$(id -g)\
-       -name "lustrec_docker" \
+docker run -it --rm \
+       --name "lustrec-from-${CONTAINER_ID}" \
        -v ${TMP_DIR}:/tmp -v ${PWD}:/home/opam/lustrec \
        ${CONTAINER_ID} $@