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

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""}