diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index df49740e..a1a4d740 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -364,6 +364,7 @@ namespace Microsoft.Boogie { }
public bool VerifySnapshots;
+ public bool VerifySeparately;
public string PrintFile = null;
public int PrintUnstructured = 0;
public int DoomStrategy = -1;
@@ -1328,7 +1329,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
- ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots)
+ ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||
+ ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately)
) {
// one of the boolean flags matched
return true;
@@ -1496,6 +1498,9 @@ namespace Microsoft.Boogie { Assign a unique ID to an implementation to be used for verification
result caching (default: ""<impl. name>:0"").
+ {:timeLimit N}
+ Set the time limit for a given implementation.
+
---- On functions ----------------------------------------------------------
{:builtin ""spec""}
@@ -1648,6 +1653,8 @@ namespace Microsoft.Boogie { /verifySnapshots
verify several program snapshots (named <filename>.v0.bpl
to <filename>.vN.bpl) using verification result caching
+ /verifySeparately
+ verify each input program separately
/removeEmptyBlocks:<c>
0 - do not remove empty blocks during VC generation
1 - remove empty blocks (default)
|