diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 667f7b7d5b694545c83369f3646dc94c023ef673..b2243fb73cbb478acf89b2041a07bc04dab24629 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,13 +11,11 @@ tests:
   script:
   - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.11.1; fi
   - eval $(opam env)
-  - opam --version
-  - opam switch
   - sudo apt-get update
   - opam repository add remote https://opam.ocaml.org
-  - opam update
+  - opam depext --yes ocplib-endian base fmt alt-ergo.2.4.0
   - opam install . --deps-only --with-test --yes
-  - opam install --yes alt-ergo.2.4.0
+  - opam install alt-ergo.2.4.0 --yes
   - make
   - make test
   tags:
diff --git a/Makefile b/Makefile
index 56837ea48581c9edabaaf468ba8e76375931c360..b9f6d170932ea621b1b18f44a6cf2747023130fd 100644
--- a/Makefile
+++ b/Makefile
@@ -7,8 +7,5 @@ test:
 promote:
 	dune promote --root=.
 
-test:
-	dune runtest
-
 clean:
 	dune clean
diff --git a/caisar.opam b/caisar.opam
index 34af71c88f6d12b6dbc71080938bd0cb50dbf362..195dfada29c8aced8f6d1971869ae2d31fdad923 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -36,5 +36,5 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 pin-depends: [
-  [ "why3" "git+https://gitlab.inria.fr/why3/why3.git#autodetection_from_file" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
 ]
diff --git a/caisar.opam.template b/caisar.opam.template
index 10174fed00800bd55414cfb2e07916a4144ba709..fd083c6da94672bdd5fee1e7e621505c51b22215 100644
--- a/caisar.opam.template
+++ b/caisar.opam.template
@@ -1,3 +1,3 @@
 pin-depends: [
-  [ "why3" "git+https://gitlab.inria.fr/why3/why3.git#autodetection_from_file" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
 ]
diff --git a/tests/simple.t b/tests/simple.t
index c8b5c220e5bccac74d6f1db27859d31285ec3235..45493a0151215a08a50567aba30b090fe681eb46 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1160,28 +1160,48 @@ Test verify
   
   function x1 [@introduced] : t19
   
+  (* meta caisar_input function x1, 0 *)
+  
   function x2 [@introduced] : t19
   
+  (* meta caisar_input function x2, 1 *)
+  
   function x3 [@introduced] : t19
   
+  (* meta caisar_input function x3, 2 *)
+  
   function x4 [@introduced] : t19
   
+  (* meta caisar_input function x4, 3 *)
+  
   function x5 [@introduced] : t19
   
+  (* meta caisar_input function x5, 4 *)
+  
   axiom H [@introduced] : lt 0.0 x1
   
   axiom H1 [@introduced] : lt x1 0.5
   
   function y : t19
   
+  (* meta caisar_output function y, 0 *)
+  
   function y1 : t19
   
+  (* meta caisar_output function y1, 1 *)
+  
   function y2 : t19
   
+  (* meta caisar_output function y2, 2 *)
+  
   function y3 : t19
   
+  (* meta caisar_output function y3, 3 *)
+  
   function y4 : t19
   
-  goal G : lt 0.0 y4 /\ lt y4 0.5
+  (* meta caisar_output function y4, 4 *)
+  
+  goal G : lt 0.0 y /\ lt y 0.5
   
   end