1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 11406dbc..5feff30a 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1906,6 +1906,13 @@ namespace Microsoft.Boogie {
        Per-implementation versions of 
        /vcsMaxCost, /vcsMaxSplits and /vcsMaxKeepGoingSplits.
 
+     {:selective_checking true}
+       Turn all asserts into assumes except for the ones reachable from
+       assumptions marked with the attribute {:start_checking_here}.
+       Thus, ""assume {:start_checking_here} something;"" becomes an inverse 
+       of ""assume false;"": the first one disables all verification before
+       it, and the second one disables all verification after.
+
   ---- On functions ----------------------------------------------------------
 
      {:bvbuiltin ""spec""}