diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-16 12:04:37 -0600 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-16 12:04:37 -0600 |
| commit | f049d2ec646244bc40964b36d961966fe2a3e4dc (patch) | |
| tree | 31dd22334b5cb314eb018fd1deee810836ffa486 /Source/ExecutionEngine | |
| parent | 74765d1b66730a612ce3eaf404883c09ab8f0153 (diff) | |
Add support for identifying unnecessary assumes.
Diffstat (limited to 'Source/ExecutionEngine')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 9623139a..9bc855be 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1008,6 +1008,11 @@ namespace Microsoft.Boogie CleanupCheckers(requestId); } + if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any()) + { + Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes)); + } + cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); outputCollector.WriteMoreOutput(); |