From 4b054873ae07725560c5d503c42e1a3adab429f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 25 Mar 2020 15:18:17 +0100
Subject: [PATCH] [wp] scripts cleanup
---
.../unsigned.0.session/script/lemma_U32.json | 8 ++++----
.../script/init_t2_bis_v2_assigns_exit_part2.json | 2 +-
.../script/init_t2_bis_v2_assigns_normal_part2.json | 2 +-
.../script/init_t2_bis_v2_loop_assigns_part2.json | 4 ++--
.../script/init_t2_v2_assigns_part2.json | 6 +++---
.../script/init_t2_v2_loop_assigns_2_part2.json | 4 ++--
.../script/init_t2_v2_loop_assigns_part2.json | 4 ++--
.../script/init_t2_v2_loop_assigns_part3.json | 4 ++--
.../script/init_t2_v3_assigns_part2.json | 6 +++---
.../script/init_t2_v3_loop_assigns_part2.json | 4 ++--
10 files changed, 22 insertions(+), 22 deletions(-)
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 5f84563cec3..c5f42638ec1 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
@@ -10,8 +10,8 @@
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
"children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid",
- "time": 0.0205,
- "steps": 14 } ],
+ "time": 0.021,
+ "steps": 12 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
"params":
@@ -27,6 +27,6 @@
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid",
- "time": 0.0201,
- "steps": 14 } ] } } ],
+ "time": 0.0189,
+ "steps": 12 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
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 fe94e71f4e3..ac9e9645d05 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
@@ -3,7 +3,7 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=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.0",
- "verdict": "valid", "time": 0.1131,
+ "verdict": "valid", "time": 0.0876,
"steps": 51 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
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 fe94e71f4e3..ac9e9645d05 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
@@ -3,7 +3,7 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=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.0",
- "verdict": "valid", "time": 0.1131,
+ "verdict": "valid", "time": 0.0876,
"steps": 51 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
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 2fdf4f699b8..dae64876176 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.7529,
- "steps": 75 } ],
+ "verdict": "valid", "time": 0.8178,
+ "steps": 88 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 61905e9c1cf..0f29709407b 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.0324,
+ "verdict": "valid", "time": 0.0318,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.4933,
- "steps": 404 } ] } } ]
+ "verdict": "valid", "time": 0.562,
+ "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 452a24b9d43..88270611f30 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.5313,
- "steps": 65 } ],
+ "verdict": "valid", "time": 0.6393,
+ "steps": 63 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 67ead11b4b8..bb9877d0ede 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.4321,
- "steps": 57 } ],
+ "verdict": "valid", "time": 0.4508,
+ "steps": 55 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 e4e625f3a14..bc59c057755 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.4321,
- "steps": 57 } ],
+ "verdict": "valid", "time": 0.4508,
+ "steps": 55 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 b857b733938..c128ee8585d 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.0324,
+ "verdict": "valid", "time": 0.0318,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.4933,
- "steps": 404 } ] } } ]
+ "verdict": "valid", "time": 0.562,
+ "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 5bbf5688947..a233cfc6311 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
@@ -3,8 +3,8 @@
"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.0",
- "verdict": "valid", "time": 0.3617,
- "steps": 72 } ],
+ "verdict": "valid", "time": 0.3477,
+ "steps": 70 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
--
GitLab