adapts the existing assertby testcases accordingly

Author: ArquintL

src/test/resources/regressions/features/assertby/assertby-proof-empty-block.gobra

@@ -7,8 +7,12 @@
 package assertbyproofemptyblock
 
 func foo(x, y int) {
+    // due to #1000, assert by proof are currently rejected by the type checker
+    //:: ExpectedOutput(type_error)
     assert true by {}
 
-    //:: ExpectedOutput(assert_by_error:assert_by_proof_body_error)
+    // due to #1000, assert by proof are currently rejected by the type checker
+    // ExpectedOutput(assert_by_error:assert_by_proof_body_error)
+    //:: ExpectedOutput(type_error)
     assert x <= y by {}
 }

src/test/resources/regressions/features/assertby/assertby-proof-fail-01.gobra

@@ -4,7 +4,9 @@
 package assertbyprooffail01
 
 func foo(x, y int) {
-    //:: ExpectedOutput(assert_by_error:assert_by_proof_body_error)
+    // due to #1000, assert by proof are currently rejected by the type checker
+    // ExpectedOutput(assert_by_error:assert_by_proof_body_error)
+    //:: ExpectedOutput(type_error)
     assert false by {
         mylemma(x, y)
     }

src/test/resources/regressions/features/assertby/assertby-proof-no-leak.gobra

@@ -7,6 +7,8 @@
 package assertbyproofnoleak
 
 func foo(x, y, z int) {
+    // due to #1000, assert by proof are currently rejected by the type checker
+    //:: ExpectedOutput(type_error)
     assert x <= y by {
         mylemma(x, y, z)
     }
@@ -15,7 +17,9 @@ func foo(x, y, z int) {
 
     // y <= z was established inside the proof block via mylemma
     // but should NOT be available here
-    //:: ExpectedOutput(assert_error:assertion_error)
+    // due to #1000, assert by proof are currently rejected by the type checker so this example does not even reach the
+    // verification phase, so the following assertion error is commented:
+    // ExpectedOutput(assert_error:assertion_error)
     assert y <= z
 }
 

src/test/resources/regressions/features/assertby/assertby-proof-simple-01.gobra

@@ -4,13 +4,17 @@
 package assertbyproofsimple01
 
 func foo(x, y int) {
+    // due to #1000, assert by proof are currently rejected by the type checker
+    //:: ExpectedOutput(type_error)
     assert x <= y by {
         mylemma(x, y)
     }
 
     assert x <= y
 
-    //:: ExpectedOutput(assert_error:assertion_error)
+    // due to #1000, assert by proof are currently rejected by the type checker so this example does not even reach the
+    // verification phase, so the following assertion error is commented:
+    // ExpectedOutput(assert_error:assertion_error)
     assert false
 }