From 53f8704021ef41d15f1ccf0d48f458781989e3ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 25 Mar 2020 16:36:12 +0100
Subject: [PATCH] [wp] update caches
---
src/plugins/wp/Makefile.in | 4 ++++
.../cache/266abf4c61d5d3612cc873cc2f658b4b.json | 2 ++
.../cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json | 2 ++
.../cache/fd2458f07a6485f7076d5a78dc65e20c.json | 2 ++
.../cache/1fe2eacd6d20f2162a4950128caf9f88.json | 2 ++
.../cache/4aed44fbe802edcf56fe979cb0bd1fd1.json | 2 ++
.../cache/756079eaf758e0a707efed015bec5bcd.json | 2 ++
.../cache/820a9cf50a575d585badbf5e5fad83a0.json | 2 ++
.../cache/875b3f59996d77e478fe981d539949d8.json | 2 ++
.../cache/91ab633347e34af327d794249d674722.json | 2 ++
.../cache/96e9a571319248796e554e1be068f1be.json | 2 ++
.../cache/b359768fc97ed1575e1a9ded31e7ed01.json | 2 ++
.../cache/b77d1b117413691fad797c4a48f3c372.json | 2 ++
.../cache/e0e8f7dccfbbe2f7426617215706e998.json | 2 ++
.../cache/e494b53ac5e3154be1b7ff4d30fa7d19.json | 2 ++
.../cache/ea44cea51e17f5beecd3c6e0bcaf6860.json | 2 ++
.../cache/f2e6496b5434869ba3461731001ad294.json | 2 ++
.../cache/f7426a5e9d31ceb59b7fe847195704e8.json | 2 ++
.../cache/034d72d9106e3380325aa1d67bc6e530.json | 2 ++
.../cache/0c30085628a552390ece72f72470887c.json | 2 ++
.../cache/45b3f3bcc0160bd4b82742281bb0a056.json | 2 ++
.../cache/70562eac8dc02df9552e2f42b8fcfda0.json | 2 ++
.../cache/abb1bf9b1f3597182f3034fa7e127544.json | 2 ++
.../cache/bb473069cb6de4ddb4a17759af940d2f.json | 2 ++
.../cache/f749942d7589b216b3eadf0150d9a3d4.json | 2 ++
.../cache/f8d02d3f4932587b1ff1da126702b1ab.json | 2 ++
.../cache/b1a18aa2a86a77a0d31483dd0650660d.json | 2 ++
.../cache/f3d86f6d80e0586d0adc5d348ad0441e.json | 1 +
.../cache/eb64f61fbab15570bb76ae4d71d1de91.json | 2 ++
.../cache/a1d76edfd7bcf43834cdac624ff86d0a.json | 1 +
30 files changed, 60 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 47549ee4316..3d55dac46a5 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -145,6 +145,10 @@ wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt
./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt
+ FRAMAC_WP_CACHE=update \
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif
+
+wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt
FRAMAC_WP_CACHE=update \
FRAMAC_WP_SCRIPT=update \
./bin/ptests.opt src/plugins/wp/tests -config qualif
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json
new file mode 100644
index 00000000000..3257442fbe4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.3682,
+ "steps": 535 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json
new file mode 100644
index 00000000000..91ef5fe08ab
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1518,
+ "steps": 166 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json
new file mode 100644
index 00000000000..638916aa4cc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2975,
+ "steps": 533 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json
new file mode 100644
index 00000000000..c20a37b337d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2665,
+ "steps": 536 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json
new file mode 100644
index 00000000000..61892a317bc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2204,
+ "steps": 567 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json
new file mode 100644
index 00000000000..82576daec3b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1849,
+ "steps": 172 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json
new file mode 100644
index 00000000000..d97aaf8bcd3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2162,
+ "steps": 539 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json
new file mode 100644
index 00000000000..196fb0c09e2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2094,
+ "steps": 557 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json
new file mode 100644
index 00000000000..7132886e0f0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1185,
+ "steps": 172 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json
new file mode 100644
index 00000000000..355e0961e4d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2524,
+ "steps": 531 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json
new file mode 100644
index 00000000000..65cfdd122a3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1041,
+ "steps": 168 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json
new file mode 100644
index 00000000000..cfff7d15506
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.212,
+ "steps": 535 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json
new file mode 100644
index 00000000000..321e3eb3df3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2572,
+ "steps": 543 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json
new file mode 100644
index 00000000000..70b6dd4b59f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1663,
+ "steps": 172 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json
new file mode 100644
index 00000000000..6d53ae41f7b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2533,
+ "steps": 535 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json
new file mode 100644
index 00000000000..b5d00d2a037
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1092,
+ "steps": 172 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json
new file mode 100644
index 00000000000..b104977442f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1496,
+ "steps": 172 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json
new file mode 100644
index 00000000000..0f49cd7ae20
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2325,
+ "steps": 551 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json
new file mode 100644
index 00000000000..d58edca4615
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 1.0112,
+ "steps": 1546 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json
new file mode 100644
index 00000000000..92b1aa4a0b5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2302,
+ "steps": 551 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json
new file mode 100644
index 00000000000..fc9a077e63d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2867,
+ "steps": 551 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json
new file mode 100644
index 00000000000..9fa2b35d47f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2475,
+ "steps": 551 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json
new file mode 100644
index 00000000000..8cf12f5ed4a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2696,
+ "steps": 551 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json
new file mode 100644
index 00000000000..06bed841ac0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.5142,
+ "steps": 1727 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json
new file mode 100644
index 00000000000..91c90a9142c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2995,
+ "steps": 551 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json
new file mode 100644
index 00000000000..a6d1470d0c4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.3396,
+ "steps": 558 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json
new file mode 100644
index 00000000000..f4fa6591e63
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "stepout", "steps": 50 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json
new file mode 100644
index 00000000000..40c36c96271
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.0239,
+ "steps": 57 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json
new file mode 100644
index 00000000000..213923a36bf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.3.0", "verdict": "timeout", "time": 10. }
--
GitLab