diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle index a0e6f10bd7a2ad26a05f087b3db5d298a17013b4..55fffbb874fe693f31443e5643dc55434b52d718 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 b504fe1c1e2b2ea8a1f509acd50fa2b3af2891c2..243ba4370ef7d85c4da9ca05a51b73719c91e0dc 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