Added an annotation, :split_here, for predicate statements.

The annotation allows the programmer to manually indicate
where the verification of a procedure implementation should be
split into pieces.

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 01212da1..682e058c 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1656,6 +1656,11 @@ namespace Microsoft.Boogie {
      {:subsumption n}

        Overrides the /subsumption command-line setting for this assertion.

 

+     {:split_here}

+       Verifies code leading to this point and code leading from this point

+       to the next split_here as separate pieces.  May help with timeouts.

+       May also occasionally double-report errors.

+

   ---- The end ---------------------------------------------------------------

 ");

     }