diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 8df080b73dbf0ccb41efe60f2e256eb3f86c0d4b..f318abf289fadf2fa603a1f23a2c77466a989011 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -31,19 +31,20 @@ Let a_20 = a_9[shift_sint32(i32_0, i)].
 Let a_21 = a_11[shift_uint32(u32_0, i)].
 Let a_22 = a_13[shift_sint64(i64_0, i)].
 Assume {
-  Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_3) /\
-      is_sint64_chunk(Mint_5) /\ is_sint8_chunk(Mchar_0) /\
-      is_uint16_chunk(Mint_2) /\ is_uint32_chunk(Mint_4) /\
-      is_uint64_chunk(Mint_6) /\ is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\
-      is_sint16_chunk(a_5) /\ is_sint32_chunk(a_9) /\
-      is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\ is_uint16_chunk(a_7) /\
-      is_uint32_chunk(a_11) /\ is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
+  Type: IsArray1_sint8(x) /\ is_sint16_chunk(Mint_1) /\
+      is_sint32_chunk(Mint_3) /\ is_sint64_chunk(Mint_5) /\
+      is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_2) /\
+      is_uint32_chunk(Mint_4) /\ is_uint64_chunk(Mint_6) /\
+      is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\ is_sint16_chunk(a_5) /\
+      is_sint32_chunk(a_9) /\ is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\
+      is_uint16_chunk(a_7) /\ is_uint32_chunk(a_11) /\
+      is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
   (* Heap *)
   Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
       (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
       (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
       (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
-      IsArray1_sint8(x) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+      linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: (0 <= i) /\ (i <= 9).
   (* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 2e93da0b17ef4d14c9bd0856053b0a18debf5b1e..0a7a16a6acadb3ef41857bbbff863c300b5da1be 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -216,16 +216,17 @@ end
     
     (* use frama_c_wp.memory.Memory *)
     
-    (* use Chunk *)
-    
     (* use S1_X *)
     
+    (* use Chunk *)
+    
     (* use Compound *)
     
     goal wp_goal :
       forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
-       addr -> int, a:addr.
+       addr -> int, a:addr, x:S1_X.
        region (base a) <= 0 ->
+       IsS1_X x ->
        is_sint16_chunk t3 ->
        is_sint32_chunk t4 ->
        is_sint8_chunk t2 ->
@@ -240,15 +241,15 @@ end
 
 Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
 Assume {
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0) /\
       IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
   (* Heap *)
   Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
       cinits(Init_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
   (* Block In *)
   Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
@@ -261,16 +262,16 @@ Prove: valid_rd(Malloc_0, p, 3).
 Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
 Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
 Assume {
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
   (* Heap *)
   Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
       cinits(Init_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
   (* Block In *)
   Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json
new file mode 100644
index 0000000000000000000000000000000000000000..bf03e943986b4885de8611be54ea04bbf995e180
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1563,
+  "steps": 286 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json
new file mode 100644
index 0000000000000000000000000000000000000000..15c20e5cfc010524d9da9cea56a6df10e5f1bc07
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0323,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json
new file mode 100644
index 0000000000000000000000000000000000000000..15c20e5cfc010524d9da9cea56a6df10e5f1bc07
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0323,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json
new file mode 100644
index 0000000000000000000000000000000000000000..79dc4338f21eab08ae04ca78c7d0d3ebcaae1cc3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0322,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json
new file mode 100644
index 0000000000000000000000000000000000000000..2172e49206ceb779b621f5c70ee8a02315e57ff5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0337,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json
new file mode 100644
index 0000000000000000000000000000000000000000..d226fb9296c30bd55af9b918488036038f75a6ae
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0377,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json
new file mode 100644
index 0000000000000000000000000000000000000000..1cb9dc9252730487f276279c07bd2478061d89b7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.138,
+  "steps": 269 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json
new file mode 100644
index 0000000000000000000000000000000000000000..d05c7f00bb2c4618af5ea65bef7521a7d3932000
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0463,
+  "steps": 123 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json
new file mode 100644
index 0000000000000000000000000000000000000000..fbd18991a8fc2a677d7fa24d46c3f57ba602a8fe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1203,
+  "steps": 252 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json
new file mode 100644
index 0000000000000000000000000000000000000000..9749d24da27964ac547d5d9ed61ad14671e2a603
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1085,
+  "steps": 235 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json
new file mode 100644
index 0000000000000000000000000000000000000000..9a8316dd72e6beba1b90c4dc201f257a994bae7c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0154,
+  "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json
new file mode 100644
index 0000000000000000000000000000000000000000..cf65d980e11860af778e7dc6762d29931eae9211
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0847,
+  "steps": 184 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json
new file mode 100644
index 0000000000000000000000000000000000000000..143a1e69e0b31c3a6308936cebbcbe926540b42f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0129,
+  "steps": 62 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json
new file mode 100644
index 0000000000000000000000000000000000000000..b2a493adaa45ed6a8227aaf072ae0e6ecaea3464
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0853,
+  "steps": 201 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json
new file mode 100644
index 0000000000000000000000000000000000000000..ef833bf2578d7f70222595dc1f1a299decc4cda1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0314,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json
new file mode 100644
index 0000000000000000000000000000000000000000..72229c47d0f66c4e493e018662c598e2b621fe6c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0722,
+  "steps": 167 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json
new file mode 100644
index 0000000000000000000000000000000000000000..ac1b7fec88fe27b0bd4194e4b68c2aa99df73e60
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0881,
+  "steps": 218 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json
new file mode 100644
index 0000000000000000000000000000000000000000..d3cae1db457b006cade45ab9c7a11d44884bf45b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0487,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json
new file mode 100644
index 0000000000000000000000000000000000000000..ac5ca13418aba9acca3c1be6d49295937c3139d9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0324,
+  "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json
new file mode 100644
index 0000000000000000000000000000000000000000..ca8a4ddf594d5e618e4499e649b2c3bcba4679c3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0096,
+  "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json
new file mode 100644
index 0000000000000000000000000000000000000000..b4eff8a25e7f98225f3c5a14eb4ce551b0c71adb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0148,
+  "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json
new file mode 100644
index 0000000000000000000000000000000000000000..e4c3de15c1aebc842360540b0be4a3a50bb7a72c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json
new file mode 100644
index 0000000000000000000000000000000000000000..5a95e44801c319dc17a99333a5cc52869ba35b50
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0079,
+  "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json
new file mode 100644
index 0000000000000000000000000000000000000000..741d4bc44f1e7e20b462777c8f3885660d53b437
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0082,
+  "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json
new file mode 100644
index 0000000000000000000000000000000000000000..e4c3de15c1aebc842360540b0be4a3a50bb7a72c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json
new file mode 100644
index 0000000000000000000000000000000000000000..e4c3de15c1aebc842360540b0be4a3a50bb7a72c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json
new file mode 100644
index 0000000000000000000000000000000000000000..e4c3de15c1aebc842360540b0be4a3a50bb7a72c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json
new file mode 100644
index 0000000000000000000000000000000000000000..066974fb6059d0d3f439d3f5596a098b88246991
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+  "steps": 35 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json
new file mode 100644
index 0000000000000000000000000000000000000000..2eb44ba21a5f5fba4f8745ad01d5fdd0df801094
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0095,
+  "steps": 52 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json
new file mode 100644
index 0000000000000000000000000000000000000000..c9b1db9c4af8b05494421e1c3baa79637bf4a247
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0181,
+  "steps": 45 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json
new file mode 100644
index 0000000000000000000000000000000000000000..a197c97ceb4be14210c464d40fa788807d00e698
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.013,
+  "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json
new file mode 100644
index 0000000000000000000000000000000000000000..c9419cd7789d6634005c87ea97b646d8cd178e3e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0115,
+  "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json
new file mode 100644
index 0000000000000000000000000000000000000000..12b29ad9f00e07f68bb55c267382888857e3be91
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0189,
+  "steps": 67 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json
new file mode 100644
index 0000000000000000000000000000000000000000..c438ee106b5facd2a15122f471bbb58d2663a762
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0118,
+  "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json
new file mode 100644
index 0000000000000000000000000000000000000000..83bedfff0270ca7834377a67c2326511706e4125
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0123,
+  "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json
new file mode 100644
index 0000000000000000000000000000000000000000..2de817ca705a2b8f74bbd67f13600afaf844d455
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0517,
+  "steps": 92 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json
new file mode 100644
index 0000000000000000000000000000000000000000..f5eb47507d00dcd4c0c201d5e27f0b1d08efc138
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+  "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json
new file mode 100644
index 0000000000000000000000000000000000000000..3291e8fc3f16fb6a8b1dbcf3ccd8d1d1376a74f8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0105,
+  "steps": 16 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json
new file mode 100644
index 0000000000000000000000000000000000000000..7416efea8d93be626b1ec83efbed764b3ab5f8db
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0254,
+  "steps": 55 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json
new file mode 100644
index 0000000000000000000000000000000000000000..b27f2eee4a798c3f0424bec879e1804e6f14ec33
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0336,
+  "steps": 178 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json
new file mode 100644
index 0000000000000000000000000000000000000000..f2ba5b4ebaeb2957efa9c2f997ff643a3b8bf6a6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0137,
+  "steps": 48 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json
new file mode 100644
index 0000000000000000000000000000000000000000..ebb299a05a873b898deeb4e9f99b6ac61c57262b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.02, "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json
new file mode 100644
index 0000000000000000000000000000000000000000..7cb834182524ff4e424912d248183d3a63132af4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0174,
+  "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json
new file mode 100644
index 0000000000000000000000000000000000000000..c16c46309855781fbcf5041df7a340a6fd6e5aef
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0159,
+  "steps": 53 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json
new file mode 100644
index 0000000000000000000000000000000000000000..084b990db485983e728e592d1e22e7352775ba0b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0102,
+  "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json
new file mode 100644
index 0000000000000000000000000000000000000000..b92d9fe95b4fdfd60dfd56f0c544de3ece1257f2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0205,
+  "steps": 62 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json
new file mode 100644
index 0000000000000000000000000000000000000000..a5593ead662d99936c212e96c1ff8e8b7806bf5e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0297,
+  "steps": 130 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json
new file mode 100644
index 0000000000000000000000000000000000000000..3fcfc93ffdf055e4738ff71fac6a2d9e9835f416
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.035,
+  "steps": 132 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json
new file mode 100644
index 0000000000000000000000000000000000000000..78e22d714721fa9b5959e2e3fbf351e155fb5afd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0285,
+  "steps": 130 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json
new file mode 100644
index 0000000000000000000000000000000000000000..ff7646a74d089cff65647aa5f89894ff8eaed89f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0113,
+  "steps": 23 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json
new file mode 100644
index 0000000000000000000000000000000000000000..c4ef5983902001e370d62ab01fb6d1bd02b0fda6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0091,
+  "steps": 39 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json
new file mode 100644
index 0000000000000000000000000000000000000000..e1e5a02eec262d90ccab8f15559834797447c353
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0198,
+  "steps": 73 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json
new file mode 100644
index 0000000000000000000000000000000000000000..e523147de7445f2fc92b08b4f2c5ad28cd413730
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0124,
+  "steps": 32 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json
new file mode 100644
index 0000000000000000000000000000000000000000..1dd11313ae1bdfa25d6357c94ab3b456e42d1b88
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0235,
+  "steps": 73 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json
new file mode 100644
index 0000000000000000000000000000000000000000..fdfc488fd363988f2a46fa39c88076115cf6c1ae
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0164,
+  "steps": 45 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json
new file mode 100644
index 0000000000000000000000000000000000000000..67801b1ad0c28ecef7c55b1f823c3a4e126fdefe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0196,
+  "steps": 71 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json
new file mode 100644
index 0000000000000000000000000000000000000000..4346351e32814ecfcf9cf27aaa8c953b79980633
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0171,
+  "steps": 53 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json
new file mode 100644
index 0000000000000000000000000000000000000000..69c84a26f331a07935e1433feca32bae056bb388
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0095,
+  "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json
new file mode 100644
index 0000000000000000000000000000000000000000..635370d75fbbd7eee02bc999018c55e06053aa13
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.016,
+  "steps": 51 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json
new file mode 100644
index 0000000000000000000000000000000000000000..2a821f8d1294a50c92c797442c707998b93813e9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.015,
+  "steps": 53 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json
new file mode 100644
index 0000000000000000000000000000000000000000..71a57ad70b2a0d6efe7e5e73d2dc89cb97c1fd5f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0078,
+  "steps": 50 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json
new file mode 100644
index 0000000000000000000000000000000000000000..5033fa63b66738bbf5a86f1d0ca29528c8f04f32
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0459,
+  "steps": 121 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json
new file mode 100644
index 0000000000000000000000000000000000000000..4b76bff9c5a623cf0f25a818753490b232ffc774
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0143,
+  "steps": 61 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json
new file mode 100644
index 0000000000000000000000000000000000000000..2ee4c477e8aabe90bed89f2bb29b95c880069d6a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.112,
+  "steps": 224 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json
new file mode 100644
index 0000000000000000000000000000000000000000..826c52aacf774cb1724cd3cf37df62c264c00e99
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0201,
+  "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json
new file mode 100644
index 0000000000000000000000000000000000000000..137bfc045d32a638b9c82843aa58f884642daed4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1581,
+  "steps": 251 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json
new file mode 100644
index 0000000000000000000000000000000000000000..7881c7c9a4564c9c68277ae070bebe1fcae4e641
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0427,
+  "steps": 101 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json
new file mode 100644
index 0000000000000000000000000000000000000000..93a6c31f0cab34a6cb804c844359d5b8041ca2e5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.027,
+  "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json
new file mode 100644
index 0000000000000000000000000000000000000000..5970963a22a590891694440fec87000dd4ab6a68
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 1.448,
+  "steps": 874 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json
new file mode 100644
index 0000000000000000000000000000000000000000..7bf27258b66983e3d60a119b305c299f4b6f6d2a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json
new file mode 100644
index 0000000000000000000000000000000000000000..1c231cee37ea3b76ac49c8f432494acf277d3336
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0123,
+  "steps": 35 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json
new file mode 100644
index 0000000000000000000000000000000000000000..e03b006e36d29d99e701dc43c186459316d2e433
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0114,
+  "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json
new file mode 100644
index 0000000000000000000000000000000000000000..7cbb165d065d1dbd07acb1d06d487f2bb5f95117
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0677,
+  "steps": 169 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json
new file mode 100644
index 0000000000000000000000000000000000000000..ca5bb4ea16033c54ec08205b8f644e5814933112
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1562,
+  "steps": 267 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json
new file mode 100644
index 0000000000000000000000000000000000000000..e667529e5baa4d3ebb31c5001d359ceadbff67f8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0207,
+  "steps": 82 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json
new file mode 100644
index 0000000000000000000000000000000000000000..34cbd0294af91f0cf248b739840a0b5ad9d40239
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0471,
+  "steps": 107 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json
new file mode 100644
index 0000000000000000000000000000000000000000..c85fd94e357708127bb8d6331b121a3c2f6842f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0372,
+  "steps": 61 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json
new file mode 100644
index 0000000000000000000000000000000000000000..b6d8db7b016fc62a5da946f54bfda917c50d555a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0262,
+  "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json
new file mode 100644
index 0000000000000000000000000000000000000000..df8ca8fe1a09a88fa5564b08e49c71584b47105d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0977,
+  "steps": 179 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json
new file mode 100644
index 0000000000000000000000000000000000000000..827ebad8defbd685d0c3d9bac65e689c99d58c62
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.2324,
+  "steps": 210 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json
new file mode 100644
index 0000000000000000000000000000000000000000..83e0ba8ee6f8168c5033ef2be8f321e4e181644e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0397,
+  "steps": 111 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json
new file mode 100644
index 0000000000000000000000000000000000000000..b1fe562c2f1fd95d589b9f712467f1cfd8ed5cc0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.02, "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json
new file mode 100644
index 0000000000000000000000000000000000000000..32f9c5fdfe9edcb7e4c5da5e0feaab1c636261c8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0193,
+  "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json
new file mode 100644
index 0000000000000000000000000000000000000000..60dab5b5ec291464cea80c17dc20b57cf182f134
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0612,
+  "steps": 151 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json
new file mode 100644
index 0000000000000000000000000000000000000000..6a103d99cdba6684393b494731f85312ada3496c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0156,
+  "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json
new file mode 100644
index 0000000000000000000000000000000000000000..83debd7e69ed104f4c81fa66a9cde382b6e0280d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0206,
+  "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json
new file mode 100644
index 0000000000000000000000000000000000000000..6e36003ddf4737497560a3ac9f8fa80e053724a2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0095,
+  "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json
new file mode 100644
index 0000000000000000000000000000000000000000..a00184de1fd2fbd11663a2bd8cb430f4b887bb97
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0574,
+  "steps": 117 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json
new file mode 100644
index 0000000000000000000000000000000000000000..9f1ee7872b4d4851deafcd9fb577e88a60b4085e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0287,
+  "steps": 93 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json
new file mode 100644
index 0000000000000000000000000000000000000000..e9844a57cba7df5ec6c0a8f2efa350c669a25a76
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0898,
+  "steps": 195 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json
new file mode 100644
index 0000000000000000000000000000000000000000..398e1b3eb8815a9b43229d7192103a6df8cb84c1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0332,
+  "steps": 95 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json
new file mode 100644
index 0000000000000000000000000000000000000000..f105ad10719cead4edcaea5b930075e62577824b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.021,
+  "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json
new file mode 100644
index 0000000000000000000000000000000000000000..2d135b932262eac686db74e68bedbba1dde0980a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+  "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json
new file mode 100644
index 0000000000000000000000000000000000000000..2471b919ea1a0651ff33d05d09ff4d43233f1830
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0233,
+  "steps": 81 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json
new file mode 100644
index 0000000000000000000000000000000000000000..ee56722a84b934902037544dc910debaa5b128b0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0305,
+  "steps": 90 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json
new file mode 100644
index 0000000000000000000000000000000000000000..ed311aa3bf7912b06da8f2e6fc4f9baf2c6e71aa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0239,
+  "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json
new file mode 100644
index 0000000000000000000000000000000000000000..19937fe629ef10a5d84d21f52fbc3235161e9e6c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.7249,
+  "steps": 586 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json
new file mode 100644
index 0000000000000000000000000000000000000000..e2adf732c23108c2c9ef96e88a482dc1e7619f8f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0076,
+  "steps": 24 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json
new file mode 100644
index 0000000000000000000000000000000000000000..453f17235fb12e7446ac059f6b9f5394cab31597
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0222,
+  "steps": 73 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json
new file mode 100644
index 0000000000000000000000000000000000000000..7181b9f0008cf5e9d8cca72f089c87247872d91c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0677,
+  "steps": 128 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json
new file mode 100644
index 0000000000000000000000000000000000000000..4ce8c833c8d25715a48213779ae3dfcec923a080
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0575,
+  "steps": 133 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json
new file mode 100644
index 0000000000000000000000000000000000000000..985a044135022550380b8c7b65d7e9930798236b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1778,
+  "steps": 240 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json
new file mode 100644
index 0000000000000000000000000000000000000000..5c8499dcc7eba207360e1808f3647efd05e845fc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0143,
+  "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json
new file mode 100644
index 0000000000000000000000000000000000000000..b480d3f35b71b962fee77381019facd24a4030fc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0856,
+  "steps": 138 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json
new file mode 100644
index 0000000000000000000000000000000000000000..e3e8779cbd7455ed9ceeb30471726da9312ebb5b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0534,
+  "steps": 114 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json
new file mode 100644
index 0000000000000000000000000000000000000000..d2cb65a7b9ede576e50197124f4f2713ba2e76b7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0333,
+  "steps": 92 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json
new file mode 100644
index 0000000000000000000000000000000000000000..1a411f445d65017ffcf9a7c804487f67a0d21693
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.023,
+  "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json
new file mode 100644
index 0000000000000000000000000000000000000000..7b78699ea7401ec5a1d97c96036db3241e153dfa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+  "steps": 28 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json
new file mode 100644
index 0000000000000000000000000000000000000000..2d31e4969e8de736681cf3f8527561bc47cc4dbe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0121,
+  "steps": 28 }
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
new file mode 100644
index 0000000000000000000000000000000000000000..428a1839b17ef04e853737e46dc2b856336d8867
--- /dev/null
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0102,
+  "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
new file mode 100644
index 0000000000000000000000000000000000000000..f6ac3dd3d95e111fc98c7f358ccec191c94976e3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0118,
+  "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json
new file mode 100644
index 0000000000000000000000000000000000000000..d3dcde5a175f470fec7ee84416474c05dc33c417
--- /dev/null
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0157,
+  "steps": 35 }