diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
new file mode 100644
index 0000000000000000000000000000000000000000..a44e4f7a5cfe5c2654916e6178f295550553a9d3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
@@ -0,0 +1,16 @@
+[ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 1 },
+ "select": { "select": "inside-step", "at": 17, "kind": "have",
+ "occur": 0, "target": "b_3 mod 2", "pattern": "%$b2" },
+ "children": { "Lower 0": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0637,
+ "steps": 96 } ],
+ "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0813,
+ "steps": 120 } ],
+ "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.3008,
+ "steps": 284 } ],
+ "Upper 1": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0965,
+ "steps": 99 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 42a2b002096f5135ea54211277cd6578cc5c70f3..92bfb254ae46eca98320c3de32493e1daf5d5130 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -10,7 +10,6 @@
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Unsuccess
[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid
@@ -21,13 +20,15 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
-[wp] Proved goals: 16 / 17
+[wp] [Script] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
+[wp] Proved goals: 17 / 17
Qed: 4
- Alt-Ergo: 12 (unsuccess: 1)
+ Script: 1
+ Alt-Ergo: 12
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 3 4 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- BinaryMultiplication 3 9 13 92.3%
+ BinaryMultiplication 3 9 13 100%
------------------------------------------------------------