diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle index a89011312ffab6b7a4b2cc2e92132cf008c533d0..93fad4096b8411cc0ee568313f9a1a9a92fadf2a 100644 --- a/tests/bugs/oracle/logiccast.res.oracle +++ b/tests/bugs/oracle/logiccast.res.oracle @@ -3,10 +3,10 @@ Now output intermediate result [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown -[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown +[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Timeout +[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Timeout [wp] Proved goals: 0 / 2 - Alt-Ergo: 0 (unknown: 2) + Alt-Ergo: 0 (interrupted: 2) [wp] Warning: Memory model hypotheses for function '_Z1mPv': /*@ behavior typed: requires \separated(&base,r+(..)); */ void _Z1mPv(void *r);