Add description of {:selective_checking} to the /attrHelp. Fix the testcase.

1 files changed, 0 insertions, 8 deletions

diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl
index 2f08618a..ed40787e 100644
--- a/Test/test2/SelectiveChecking.bpl
+++ b/Test/test2/SelectiveChecking.bpl
@@ -1,11 +1,3 @@
-/*
-In functions marked with {:selective_checking} all asserts are turned into assumes,
-except for the ones reachable from the commands marked with {:start_checking_here}.
-Thus, "assume {:start_checking_here} whatever;" is an inverse of "assume false;".
-The first one disables all verification before it, and the second one disables
-all verification after.
-*/
-
 procedure {:selective_checking} foo()
 {
   var x, y, z : int;