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
index 84122113e4f6f71c099b879fa46b335a52e7d039..0778557e77c2c2150fdde7c8446cf06c3190a7f2 100644
--- 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
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid", "time": 1.13, "steps": 65987 },
- { "header": "Range", "tactic": "Wp.range",
+[ { "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" },
@@ -11,11 +10,11 @@
"pattern": "to_uint64.2$x" },
"children": { "In-Range": [ { "prover": "CVC4:1.7",
"verdict": "valid",
- "time": 0.04,
+ "time": 0.05,
"steps": 9937 } ],
"No-Overflow": [ { "prover": "CVC4:1.7",
"verdict": "valid",
- "time": 0.04,
+ "time": 0.05,
"steps": 9890 } ] } } ],
"Value 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
@@ -30,7 +29,7 @@
"steps": 8691 } ],
"No-Overflow": [ { "prover": "CVC4:1.7",
"verdict": "valid",
- "time": 1.13,
+ "time": 1.07,
"steps": 65987 } ] } } ],
"Value 1": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
@@ -45,8 +44,8 @@
"steps": 8794 } ],
"No-Overflow": [ { "prover": "CVC4:1.7",
"verdict": "valid",
- "time": 0.34,
+ "time": 0.31,
"steps": 54186 } ] } } ],
- "Upper 1": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.0919,
+ "Upper 1": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.085,
"steps": 60 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index 8811d9b8a7870662da27cba68dfb26538d785553..55350f0445be60ba5d6b9032fc0dba0da6e99feb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -1,7 +1,7 @@
----------------------------------------------------------
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
-1. The Alt-Ergo theorem prover, version 2.3.3
+1. The Alt-Ergo theorem prover, version 2.3.1
2. The Why3 platform, version 1.3.3
3. The Coq Proof Assistant, version 8.12.0
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 698f70e328189bd1eb4f62ef7aecae1588846a22..9856a0f8ecb926f1732c110ebb67f2a81d73e3b9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.3.3'
+[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.3.1'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
index b5bf8ebae8688cf7e111e29ea2f31fc33a4a91ea..935e651c557a113872f0928ef991a381b9d3189b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
@@ -8,10 +8,10 @@
"select": { "select": "clause-goal",
"target": "(0<=x_0) /\\ (0<=(land 4294967295 x_0)) /\\ (x_0<=4294967295)",
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
- "children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.0.0",
+ "children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "valid",
- "time": 0.0101,
- "steps": 10 } ],
+ "time": 0.0111,
+ "steps": 12 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
"params":
@@ -25,8 +25,8 @@
{ "bit-range":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
- "Goal 3/3": [ { "prover": "Alt-Ergo:2.0.0",
+ "Goal 3/3": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "valid",
- "time": 0.0095,
- "steps": 10 } ] } } ],
+ "time": 0.0081,
+ "steps": 12 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 71e7e7740fd6dc473fad791e41591bbf0d4e1a41..4dc2d8b6cabcc2b77ac16615387e15dadd33c4a1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,7 +2,6 @@
[kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] Warning: Prover 'Alt-Ergo:2.0.0' not found, fallback to 'Alt-Ergo:2.3.3'
[wp] [Script] Goal typed_lemma_U32 : Valid
[wp] Proved goals: 1 / 1
Qed: 0
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index 9911b3686e49e0e234d76cf467afc93d72e5c556..197e7438b29be47c049019971e2c99a3bef4ea6b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.045,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.0428,
"steps": 51 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 5.0297,
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 4.5229,
"steps": 1538 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index 9911b3686e49e0e234d76cf467afc93d72e5c556..197e7438b29be47c049019971e2c99a3bef4ea6b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.045,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.0428,
"steps": 51 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 5.0297,
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 4.5229,
"steps": 1538 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index 6efa3dc36e291a9556b1549d86caea429b163d63..dbe20251861305ea9291e0d46d0f3cc40aa9ba83 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -2,10 +2,10 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.3644,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.3091,
"steps": 88 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index 3619f34beef6fa4bbb9518452f6fd2e02f6a9671..f1c076f5eb5471bf541995ff82f61879c61684e6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -2,7 +2,7 @@
"select": { "select": "clause-goal",
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 19 },
@@ -53,7 +53,7 @@
"verdict": "valid" } ],
"Upper 19": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
index 969d6ae1b0408a44dc97cfd8eb69e5f70f90d8fc..41b373a6e54e8b6231b666190e910c95a7151674 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.0185,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.0209,
"steps": 39 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.3353,
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.3847,
"steps": 414 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 5ff21f52dac52c63ed6e2b23cd6c9e5bad36a3c6..e8476b2bd1c63522d43203e4e126ceaf273515cf 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -2,10 +2,10 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.2526,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.3278,
"steps": 63 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index 01799509bc0fd405cd16e8a4cf21ab556b887a03..7f0e672f485fb80e567ce6bfdbdaa7422b513d53 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -2,7 +2,7 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 19 },
@@ -53,7 +53,7 @@
"verdict": "valid" } ],
"Upper 19": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index 3fce2e67b7d402ec75a3f4d80e88104eb487dd12..66e344277fc56cfd90afd1b0cb010bba08652476 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -2,10 +2,10 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.2334,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.268,
"steps": 55 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index 03c17f6ac0796117ba717d85930b869413f80a1c..188cfcd42fcb141ebf66ecda41ec53177b46cb0c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -2,10 +2,10 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.2334,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.268,
"steps": 55 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
index 3cb5eb6b507b6d657fd827eab77d60730cfcf3ea..17c80315d7b3de1e575a536192bb50d68594352a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.0185,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.0209,
"steps": 39 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.3353,
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.3847,
"steps": 414 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index 3e4b48e9eaaf0e02187fa2b7a5f5068b0072d6d3..a19acdbd05d02f92b825d79c61720359318e9edc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -2,10 +2,10 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
- "verdict": "valid", "time": 0.2263,
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
+ "verdict": "valid", "time": 0.2442,
"steps": 70 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index e668e596d9900706eb7344d109e60e683dd7fc47..f1e86438c2ee6126806723824b1b68c08fe6a741 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -2,7 +2,7 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 19 },
@@ -53,7 +53,7 @@
"verdict": "valid" } ],
"Upper 19": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.3",
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.1",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 9 },