Added clarification to function_check_05 test.

Author: klaas

regression/contracts/function_check_05/main.c

@@ -10,7 +10,9 @@ __CPROVER_ensures(__CPROVER_return_value == 1)
 int main() {
   int y = 0;  
   int z = foo(&y);
+  // This assert should fail.
   assert(y == 0);
+  // This one should succeed.
   assert(z == 1);
   return 0;
 }

regression/contracts/function_check_05/test.desc

@@ -1,8 +1,8 @@
 KNOWNBUG # Contract checking does not properly havoc function calls
 main.c
 --check-code-contracts
-^\[main.assertion.1\] assertion x == 0: FAILURE$
-^\[main.assertion.2\] assertion y == 1: SUCCESS$
+^\[main.assertion.1\] assertion y == 0: FAILURE$
+^\[main.assertion.2\] assertion z == 1: SUCCESS$
 ^\[foo.1\] : SUCCESS$
 
 ^VERIFICATION SUCCESSFUL$