summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-10-12 01:18:45 +0000
committerGravatar MichalMoskal <unknown>2010-10-12 01:18:45 +0000
commit45fb2f73118bf4010ad08757122d829c76e676d3 (patch)
treee67f8006ad0e4a72f6fb2340ae14e6716452fe4d /Source/BoogieDriver
parent2b1ddfbe8bcd48da4cab27e06078de59eecc8f40 (diff)
Make the -mv option use the new Model class.
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 33b9146c..0fc67e15 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -642,7 +642,7 @@ namespace Microsoft.Boogie {
Console.WriteLine("Execution trace:");
error.Print(4);
}
- if (CommandLineOptions.Clo.ModelView == 1) {
+ if (CommandLineOptions.Clo.ModelViewFile != null) {
error.PrintModel();
}
errorCount++;