From 22acbd3758f10f8b257f0ab0cca1630ed452756d Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 28 Aug 2020 11:28:07 +0200 Subject: [PATCH] [tests] update oracle now that WP uses cache --- tests/bugs/oracle/issue24.res.oracle | 8 ++++---- tests/bugs/oracle/issue27-pred.res.oracle | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle index a0e6f10b..55fffbb8 100644 --- a/tests/bugs/oracle/issue24.res.oracle +++ b/tests/bugs/oracle/issue24.res.oracle @@ -6,10 +6,10 @@ Now output intermediate result [wp] 6 goals scheduled [wp] [Qed] Goal typed_Z1m_assert_4 : Valid [wp] [Qed] Goal typed_Z1m_assert_5 : Valid -[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid (unqualified) -[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid (unqualified) -[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid (unqualified) -[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid (unqualified) +[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid +[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid +[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid +[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid [wp] Proved goals: 6 / 6 Qed: 2 Alt-Ergo: 4 diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle index b504fe1c..243ba437 100644 --- a/tests/bugs/oracle/issue27-pred.res.oracle +++ b/tests/bugs/oracle/issue27-pred.res.oracle @@ -4,8 +4,8 @@ Now output intermediate result [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled +[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid [wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid -[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid (unqualified) [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -- GitLab