diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/081f176e0fb3514fde320ca30f2ed032.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/081f176e0fb3514fde320ca30f2ed032.json
new file mode 100644
index 0000000000000000000000000000000000000000..f41cd911559d54336ad2c2401cfa94f24b7eff43
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/081f176e0fb3514fde320ca30f2ed032.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0233,
+  "steps": 69 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/18d8398601f0b7f85e551f1c1d9137df.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/18d8398601f0b7f85e551f1c1d9137df.json
new file mode 100644
index 0000000000000000000000000000000000000000..789606551ae1568223698632712ded58e344eaba
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/18d8398601f0b7f85e551f1c1d9137df.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0126,
+  "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/257633c0e6e4c90dbbb56430d547f891.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/257633c0e6e4c90dbbb56430d547f891.json
new file mode 100644
index 0000000000000000000000000000000000000000..19298929ccfa010c30a3962678acbed928e32500
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/257633c0e6e4c90dbbb56430d547f891.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0125,
+  "steps": 58 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2ba9be92a508348223e7c319004017c5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2ba9be92a508348223e7c319004017c5.json
new file mode 100644
index 0000000000000000000000000000000000000000..ee671250c0f2c53dc1dedaa2468422927fc0b605
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2ba9be92a508348223e7c319004017c5.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0812,
+  "steps": 221 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2c3c7fa586fc9ecea4bbf0fb98aa925f.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2c3c7fa586fc9ecea4bbf0fb98aa925f.json
new file mode 100644
index 0000000000000000000000000000000000000000..ae56e7704a656c79fff8d4c4d0ed2e557505d744
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2c3c7fa586fc9ecea4bbf0fb98aa925f.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0062,
+  "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/34f0cce3d0a30b5a3b6408ef7e1f66dd.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/34f0cce3d0a30b5a3b6408ef7e1f66dd.json
new file mode 100644
index 0000000000000000000000000000000000000000..6903eb2790ac9e6c3737e1191da741bbaeb40e2c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/34f0cce3d0a30b5a3b6408ef7e1f66dd.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0108,
+  "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3974383ae185871e55bfcf7246735ec2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3974383ae185871e55bfcf7246735ec2.json
new file mode 100644
index 0000000000000000000000000000000000000000..7bf1547019b915cc7fabd099466ec2af99a2e691
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3974383ae185871e55bfcf7246735ec2.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0194,
+  "steps": 61 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3adced65475fd2200b005fdcdd713dc3.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3adced65475fd2200b005fdcdd713dc3.json
new file mode 100644
index 0000000000000000000000000000000000000000..26695d4bb89895b0c9a45f7cc26684c0d8c73c1e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3adced65475fd2200b005fdcdd713dc3.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0102,
+  "steps": 41 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/51b6e40bd79f42701fd59c85017e8c67.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/51b6e40bd79f42701fd59c85017e8c67.json
new file mode 100644
index 0000000000000000000000000000000000000000..4256c5bdfa458cda5dd5451fceb92cc5f34bbd3a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/51b6e40bd79f42701fd59c85017e8c67.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0278,
+  "steps": 106 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/5ac49d42d9ca3323758823bcf455a64a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/5ac49d42d9ca3323758823bcf455a64a.json
new file mode 100644
index 0000000000000000000000000000000000000000..d7d50229deb8bbe91c04b3bd40c5d10f50284246
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/5ac49d42d9ca3323758823bcf455a64a.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0084,
+  "steps": 20 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/76c334c73d313cc80db5f546c34b680a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/76c334c73d313cc80db5f546c34b680a.json
new file mode 100644
index 0000000000000000000000000000000000000000..ad80acda5455f1f302b2498b886d2381f63a0fd1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/76c334c73d313cc80db5f546c34b680a.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0237,
+  "steps": 79 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/78d3c10c9f4d515da47f9cfa8cd5f089.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/78d3c10c9f4d515da47f9cfa8cd5f089.json
new file mode 100644
index 0000000000000000000000000000000000000000..0aa23b3e4ffbc87adc32a9b7c73d1602f49a3afe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/78d3c10c9f4d515da47f9cfa8cd5f089.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0055,
+  "steps": 13 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/7d831c16cfa87e08b115470eafa6f297.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/7d831c16cfa87e08b115470eafa6f297.json
new file mode 100644
index 0000000000000000000000000000000000000000..4674d99de6ef42aa3784f3eb928477da7c44dc21
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/7d831c16cfa87e08b115470eafa6f297.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0094,
+  "steps": 45 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/8b7a4ef053798c5fe79c2441519c622c.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/8b7a4ef053798c5fe79c2441519c622c.json
new file mode 100644
index 0000000000000000000000000000000000000000..6ca41aaf838c6f2cb0993d8ace5c3dc637980256
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/8b7a4ef053798c5fe79c2441519c622c.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0103,
+  "steps": 47 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/90c73ba96bd8257920ff21223c812125.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/90c73ba96bd8257920ff21223c812125.json
new file mode 100644
index 0000000000000000000000000000000000000000..3ca1f1cbaed98597111b06cb34a5b9819d0b7725
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/90c73ba96bd8257920ff21223c812125.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0088,
+  "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/98854ec13622e5ec44ff5b7522d9f26f.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/98854ec13622e5ec44ff5b7522d9f26f.json
new file mode 100644
index 0000000000000000000000000000000000000000..0f6a74b7019a529a9e0646100d47e29871a9e8af
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/98854ec13622e5ec44ff5b7522d9f26f.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.03,
+  "steps": 120 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/9c5eb1b10b9b274dd4fbf3d5e8df3d69.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/9c5eb1b10b9b274dd4fbf3d5e8df3d69.json
new file mode 100644
index 0000000000000000000000000000000000000000..39faa832aa60c68bcc94d067a0e695cd7d667ff9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/9c5eb1b10b9b274dd4fbf3d5e8df3d69.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.009,
+  "steps": 36 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b56e7d6a235dddcbe29f1c51a381822d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b56e7d6a235dddcbe29f1c51a381822d.json
new file mode 100644
index 0000000000000000000000000000000000000000..173d4b03cd0f8d5df8e3c57bdb066b05a9363ae2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b56e7d6a235dddcbe29f1c51a381822d.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0108,
+  "steps": 12 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b6afdfbe4387f23f76c81fce157d51f3.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b6afdfbe4387f23f76c81fce157d51f3.json
new file mode 100644
index 0000000000000000000000000000000000000000..daa14e99bc68b4bc436208f688f43f1d462c918e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b6afdfbe4387f23f76c81fce157d51f3.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0067,
+  "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b76b85cb9cbd9414da673bb5c9301198.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b76b85cb9cbd9414da673bb5c9301198.json
new file mode 100644
index 0000000000000000000000000000000000000000..39f6d3686a8c424d30bea1fc0c8c8790e836ebaf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/b76b85cb9cbd9414da673bb5c9301198.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0088,
+  "steps": 14 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/bb5b3a4b9614a0ac7a50ca1e478100f2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/bb5b3a4b9614a0ac7a50ca1e478100f2.json
new file mode 100644
index 0000000000000000000000000000000000000000..409944cab7b1a87c362f99fa74a268bfc42eecbf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/bb5b3a4b9614a0ac7a50ca1e478100f2.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0045,
+  "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/c79c741d0e84bd4d040c657384652af3.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/c79c741d0e84bd4d040c657384652af3.json
new file mode 100644
index 0000000000000000000000000000000000000000..89bd066ef2674b0ce7b41151392ada9edfea4a03
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/c79c741d0e84bd4d040c657384652af3.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.034,
+  "steps": 177 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/ce1bee755612ba7d4da4f1f95a9aad0e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/ce1bee755612ba7d4da4f1f95a9aad0e.json
new file mode 100644
index 0000000000000000000000000000000000000000..34492f8c7fe8dce9071d3788b7df47913e8ef70d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/ce1bee755612ba7d4da4f1f95a9aad0e.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0112,
+  "steps": 13 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/cf73637f2664f7955b6e923819b19f5b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/cf73637f2664f7955b6e923819b19f5b.json
new file mode 100644
index 0000000000000000000000000000000000000000..3a95f7af6fabb8d6c659d72a41cf0b4446624f51
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/cf73637f2664f7955b6e923819b19f5b.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.011,
+  "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e2edd396aad35ff5ad42c24b1b0ee563.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e2edd396aad35ff5ad42c24b1b0ee563.json
new file mode 100644
index 0000000000000000000000000000000000000000..ae78eafb8924e35134def7f74205351bdd66ca08
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e2edd396aad35ff5ad42c24b1b0ee563.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0155,
+  "steps": 30 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e9bdbed0b3fe4001efaf91559cb6d9d9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e9bdbed0b3fe4001efaf91559cb6d9d9.json
new file mode 100644
index 0000000000000000000000000000000000000000..7483bd33c39345c4719e78a8a45917a103288c57
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e9bdbed0b3fe4001efaf91559cb6d9d9.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0104,
+  "steps": 14 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/ed1e3bb2fcca87006f6dcd1df31d8156.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/ed1e3bb2fcca87006f6dcd1df31d8156.json
new file mode 100644
index 0000000000000000000000000000000000000000..8dd9c590e2c931ab8450134f33a3cc15b9c2f069
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/ed1e3bb2fcca87006f6dcd1df31d8156.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0192,
+  "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/f119bd195b4d894e956c342e58c068db.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/f119bd195b4d894e956c342e58c068db.json
new file mode 100644
index 0000000000000000000000000000000000000000..107ce5c3bd42fb74717d8c1e06d67218a455bb42
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/f119bd195b4d894e956c342e58c068db.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0035,
+  "steps": 32 }