From c6c815a8ddb80eb4e43714a6223bd8e5c7687a74 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Thu, 13 Jan 2011 02:46:19 +0000
Subject: Add description of {:selective_checking} to the /attrHelp. Fix the
 testcase.

---
 Test/test2/SelectiveChecking.bpl | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'Test/test2')

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;
-- 
cgit v1.2.3