From 58aebd88c0c237f8f4372e7f001f12220d2e2ce0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 17 Oct 2019 11:22:56 +0200
Subject: [PATCH] [qed+wp] fix typo in inductive types for native coq
---
.../wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle | 3 ++-
.../cache/73ea306163d25a228b4586b8b98472f6.json | 1 +
2 files changed, 3 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.session/cache/73ea306163d25a228b4586b8b98472f6.json
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
index 98f16227983..496e2f06900 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
@@ -4,8 +4,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [Failed] Goal typed_foo_assert_ko
+[wp] [Alt-Ergo 2.0.0] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1
+ Alt-Ergo 2.0.0: 0 (unsuccess: 1)
[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2471.0.report.json'
[wp] Report out: 'tests/wp_bts/result_qualif/bts_2471.0.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.session/cache/73ea306163d25a228b4586b8b98472f6.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.session/cache/73ea306163d25a228b4586b8b98472f6.json
new file mode 100644
index 00000000000..852d81aab27
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.session/cache/73ea306163d25a228b4586b8b98472f6.json
@@ -0,0 +1 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 1. }
--
GitLab