summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar 0biha <unknown>2014-12-26 16:53:41 +0100
committerGravatar 0biha <unknown>2014-12-26 16:53:41 +0100
commitf87d1d077824dc7a8c1d198b8e54d262c3937b77 (patch)
treec1433df6d1c85ead5490f9771c485a6ea6bcd62b /Source/Core
parent836c533eb0b1147d50f91f5ed5138b6abff270f9 (diff)
parent94c192b6e706fd296bae7d08fecab8dbc9592172 (diff)
Merge
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/CommandLineOptions.cs5
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 ---------------------------------------------------------------
");
}