From 8c604f7ad692723a9e97d83f475f484446ff3441 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 2 Oct 2020 13:23:52 +0200
Subject: [PATCH] [wp] update scripts with alt-ergo 2.3.1
---
...lication_loop_invariant_inv1_ok_preserved.json | 15 +++++++--------
.../wp_plugin/oracle_qualif/config.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/fallback.res.oracle | 2 +-
.../unsigned.0.session/script/lemma_U32.json | 12 ++++++------
.../wp_plugin/oracle_qualif/unsigned.res.oracle | 1 -
.../script/init_t2_bis_v2_assigns_exit_part2.json | 8 ++++----
.../init_t2_bis_v2_assigns_normal_part2.json | 8 ++++----
.../script/init_t2_bis_v2_loop_assigns_part2.json | 6 +++---
.../script/init_t2_bis_v2_loop_assigns_part3.json | 4 ++--
.../script/init_t2_v2_assigns_part2.json | 8 ++++----
.../script/init_t2_v2_loop_assigns_2_part2.json | 6 +++---
.../script/init_t2_v2_loop_assigns_2_part3.json | 4 ++--
.../script/init_t2_v2_loop_assigns_part2.json | 6 +++---
.../script/init_t2_v2_loop_assigns_part3.json | 6 +++---
.../script/init_t2_v3_assigns_part2.json | 8 ++++----
.../script/init_t2_v3_loop_assigns_part2.json | 6 +++---
.../script/init_t2_v3_loop_assigns_part3.json | 4 ++--
17 files changed, 52 insertions(+), 54 deletions(-)
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 84122113e4f..0778557e77c 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 8811d9b8a78..55350f0445b 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 698f70e3281..9856a0f8ecb 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 b5bf8ebae86..935e651c557 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 71e7e7740fd..4dc2d8b6cab 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 9911b3686e4..197e7438b29 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 9911b3686e4..197e7438b29 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 6efa3dc36e2..dbe20251861 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 3619f34beef..f1c076f5eb5 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 969d6ae1b04..41b373a6e54 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 5ff21f52dac..e8476b2bd1c 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 01799509bc0..7f0e672f485 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 3fce2e67b7d..66e344277fc 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 03c17f6ac07..188cfcd42fc 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 3cb5eb6b507..17c80315d7b 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 3e4b48e9eaa..a19acdbd05d 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 e668e596d99..f1e86438c2e 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 },
--
GitLab