From f4a262361cbf2f363907c5ef31c22f08f1b0c77a Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 12 Jan 2021 08:50:24 +0100
Subject: [PATCH] [WP] updates json script files
---
.../script/init_t2_bis_v2_assigns_exit_part2.json | 4 ++--
.../script/init_t2_bis_v2_assigns_normal_part2.json | 4 ++--
.../script/init_t2_bis_v2_loop_assigns_part2.json | 4 ++--
.../script/init_t2_bis_v2_loop_assigns_part3.json | 4 ++--
4 files changed, 8 insertions(+), 8 deletions(-)
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 e2661ac0ea5..139c4b84bd1 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,8 +3,8 @@
"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$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.017,
+ "verdict": "valid", "time": 0.0072,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0148,
+ "verdict": "valid", "time": 0.0051,
"steps": 22 } ] } } ]
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 e2661ac0ea5..139c4b84bd1 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,8 +3,8 @@
"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$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.017,
+ "verdict": "valid", "time": 0.0072,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0148,
+ "verdict": "valid", "time": 0.0051,
"steps": 22 } ] } } ]
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 347be3b9000..df90f71b8c9 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$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0241,
+ "verdict": "valid", "time": 0.0151,
"steps": 41 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.025,
+ "verdict": "valid", "time": 0.0147,
"steps": 41 } ] } } ]
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 a5416d5a156..ab6c0d166bb 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
@@ -3,8 +3,8 @@
"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$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0199,
+ "verdict": "valid", "time": 0.0115,
"steps": 29 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0241,
+ "verdict": "valid", "time": 0.0117,
"steps": 29 } ] } } ]
--
GitLab