From 0af0a459f5f2d9db83fe8bc6cfb1a0a56aff21e7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 22 Aug 2023 21:48:01 +0200
Subject: [PATCH] Fixed test annotations

---
 tests/functional/verification/issues/00024.py | 7 -------
 tests/functional/verification/issues/00074.py | 8 ++++----
 tests/functional/verification/issues/00150.py | 2 +-
 3 files changed, 5 insertions(+), 12 deletions(-)
 delete mode 100644 tests/functional/verification/issues/00024.py

diff --git a/tests/functional/verification/issues/00024.py b/tests/functional/verification/issues/00024.py
deleted file mode 100644
index 1e8f7957..00000000
--- a/tests/functional/verification/issues/00024.py
+++ /dev/null
@@ -1,7 +0,0 @@
-# Any copyright is dedicated to the Public Domain.
-# http://creativecommons.org/publicdomain/zero/1.0/
-
-
-def bla() -> None:
-    #:: ExpectedOutput(type.error:Cannot resolve name "a" (possible cyclic definition))
-    a = a
\ No newline at end of file
diff --git a/tests/functional/verification/issues/00074.py b/tests/functional/verification/issues/00074.py
index 5496fb73..ab5ffc9c 100644
--- a/tests/functional/verification/issues/00074.py
+++ b/tests/functional/verification/issues/00074.py
@@ -7,15 +7,15 @@
 
 class Super:
 
-    #:: Label(L1)
     def foo(self, *args: Tuple[int]) -> int:
         Requires(len(args) > 3)
+        #:: ExpectedOutput(postcondition.violated:assertion.false,L1)
         Ensures(Result() > 2)
         return 5
 
-    #:: Label(L2)
     def bar(self, **kwargs: Dict[str, int]) -> int:
         Requires(len(kwargs) > 3)
+        #:: ExpectedOutput(postcondition.violated:assertion.false,L2)
         Ensures(Result() > 2)
         return 5
 
@@ -35,14 +35,14 @@ def bar(self, **kwargs: Dict[str, int]) -> int:
 
 class Sub2(Super):
 
+    #:: Label(L1)
     def foo(self, *args: Tuple[int]) -> int:
         Requires(len(args) > 2)
-        #:: ExpectedOutput(postcondition.violated:assertion.false,L1)
         Ensures(Result() > 0)
         return 5
 
+    #:: Label(L2)
     def bar(self, **kwargs: Dict[str, int]) -> int:
         Requires(len(kwargs) > 2)
-        #:: ExpectedOutput(postcondition.violated:assertion.false,L2)
         Ensures(Result() > 0)
         return 5
diff --git a/tests/functional/verification/issues/00150.py b/tests/functional/verification/issues/00150.py
index bc2d4b48..019de2af 100644
--- a/tests/functional/verification/issues/00150.py
+++ b/tests/functional/verification/issues/00150.py
@@ -21,7 +21,7 @@ def can_node_be_compressed(marked_execution_tree: 'Node') -> int:
     Requires(Forall(int, lambda i: Implies(i >= 0 and i < len(marked_execution_tree.children),
                                            Acc(marked_execution_tree.children[i].function_name))))
     Requires(Acc(marked_execution_tree.function_name))
-    #:: ExpectedOutput(postcondition.violdated:assertion.false)
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
     Ensures(Implies(len(marked_execution_tree.children) != 1, Result() == 0))
     Ensures(Result() == 0)
     if len(marked_execution_tree.children) != 1: