From 910a5a252cfaffe67b16d7a54d12418d62df49d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 22 Jan 2020 09:27:58 +0100
Subject: [PATCH] [wp] cache updates

---
 .../equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json | 2 ++
 .../equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json | 2 ++
 .../equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json | 2 ++
 .../cache/c74996e8ecbe3a35835609127c6e2b4e.json                 | 2 ++
 .../cache/2ba962f82cf233aaa33bee4e5a4ef868.json                 | 2 ++
 .../cache/79eb15660c78742aed7621a6dd68b527.json                 | 2 ++
 .../cache/62ebc7446153c03392e768f156775a04.json                 | 2 ++
 .../cache/f4a2b5ec3ce22173881bed69a80a352d.json                 | 2 ++
 .../cache/108580f3feacdb8f5c76cbe017d6adc4.json                 | 2 ++
 .../frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json | 1 +
 .../frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json | 2 ++
 .../frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json | 2 ++
 12 files changed, 23 insertions(+)
 create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json
 create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json
 create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json
 create mode 100644 src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json
 create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json
 create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json
 create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json
 create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json
 create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json
 create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json
 create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json
 create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json

diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json
new file mode 100644
index 00000000000..8ab93056803
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0163,
+  "steps": 26 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json
new file mode 100644
index 00000000000..8f61a59ddf5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0164,
+  "steps": 9 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json
new file mode 100644
index 00000000000..b81312cd959
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0102,
+  "steps": 12 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json
new file mode 100644
index 00000000000..e61b1e99569
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0126,
+  "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json
new file mode 100644
index 00000000000..cb6217f3a67
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0186,
+  "steps": 23 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json
new file mode 100644
index 00000000000..e886fc370aa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0225,
+  "steps": 34 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json
new file mode 100644
index 00000000000..66a7393b502
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0178,
+  "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json
new file mode 100644
index 00000000000..d6ed629ed65
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0175,
+  "steps": 23 }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json
new file mode 100644
index 00000000000..b068113a500
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0225,
+  "steps": 44 }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json
new file mode 100644
index 00000000000..16d19ceb388
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json
@@ -0,0 +1 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json
new file mode 100644
index 00000000000..17b2892ccbf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0111,
+  "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json
new file mode 100644
index 00000000000..ebe158e7461
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0144,
+  "steps": 16 }
-- 
GitLab