new script for wp_gallery/binary-multiplication

src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json

+[ { "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 } ] } } ]

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%
 ------------------------------------------------------------