From 5a119396e389680292c49121215e0bdb496e1794 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 May 2020 11:45:24 +0200
Subject: [PATCH] [wp] cache & script update
---
.../cache/1bb537c78b8c75937146b054d82dcc18.json | 3 +--
.../cache/284a5858dd64443846fc65ac65529167.json | 2 --
.../cache/45b4321404dd1cb2353aba38b0fbe37d.json | 3 +--
.../cache/493c0fe01cbc4d37ef3d43ec817ce6c1.json | 2 --
.../cache/a85c519ac770748cb6c297b0f4299ac4.json | 2 ++
.../cache/f68661d77a8a5cf449601b04c2baf536.json | 2 ++
.../unsigned.0.session/script/lemma_U32.json | 12 ++++++------
7 files changed, 12 insertions(+), 14 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/284a5858dd64443846fc65ac65529167.json
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/493c0fe01cbc4d37ef3d43ec817ce6c1.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/a85c519ac770748cb6c297b0f4299ac4.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/f68661d77a8a5cf449601b04c2baf536.json
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/1bb537c78b8c75937146b054d82dcc18.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/1bb537c78b8c75937146b054d82dcc18.json
index 87a46c3c9a7..629ee447710 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/1bb537c78b8c75937146b054d82dcc18.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/1bb537c78b8c75937146b054d82dcc18.json
@@ -1,2 +1 @@
-{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.0189,
- "steps": 12 }
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "failed" }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/284a5858dd64443846fc65ac65529167.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/284a5858dd64443846fc65ac65529167.json
deleted file mode 100644
index f0e350253ee..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/284a5858dd64443846fc65ac65529167.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.0205,
- "steps": 14 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/45b4321404dd1cb2353aba38b0fbe37d.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/45b4321404dd1cb2353aba38b0fbe37d.json
index 4f32c22c7c1..629ee447710 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/45b4321404dd1cb2353aba38b0fbe37d.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/45b4321404dd1cb2353aba38b0fbe37d.json
@@ -1,2 +1 @@
-{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.021,
- "steps": 12 }
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "failed" }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/493c0fe01cbc4d37ef3d43ec817ce6c1.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/493c0fe01cbc4d37ef3d43ec817ce6c1.json
deleted file mode 100644
index 782bc2de2e6..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/493c0fe01cbc4d37ef3d43ec817ce6c1.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.0201,
- "steps": 14 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/a85c519ac770748cb6c297b0f4299ac4.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/a85c519ac770748cb6c297b0f4299ac4.json
new file mode 100644
index 00000000000..70689e8559b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/a85c519ac770748cb6c297b0f4299ac4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.011,
+ "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/f68661d77a8a5cf449601b04c2baf536.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/f68661d77a8a5cf449601b04c2baf536.json
new file mode 100644
index 00000000000..741d4bc44f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/cache/f68661d77a8a5cf449601b04c2baf536.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0082,
+ "steps": 10 }
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 c5f42638ec1..2aeaa6d374e 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.3.0",
+ "children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid",
- "time": 0.021,
- "steps": 12 } ],
+ "time": 0.011,
+ "steps": 10 } ],
"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.3.0",
+ "Goal 3/3": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid",
- "time": 0.0189,
- "steps": 12 } ] } } ],
+ "time": 0.0082,
+ "steps": 10 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
--
GitLab