Boogie:

* Added /mv flag as the start of a Boogie replacement for /cev
* Allow attributes on assume statements
* /mv looks for the assume-statement attribute :captureState with a string-literal argument

1 files changed, 3 insertions, 0 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index a0005263..b4798299 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -731,6 +731,9 @@ namespace Microsoft.Boogie {
                     Console.WriteLine("Execution trace:");

                     error.Print(4);

                   }

+                  if (CommandLineOptions.Clo.ModelView == 1) {

+                    error.PrintModel();

+                  }

                   errorCount++;

                 }

                 //}