From 715b21620d5e810b03a2f7cdeb2d8d7070bd70ef Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@microsoft.com>
Date: Mon, 27 Oct 2014 14:13:17 -0700
Subject: Add support for counting spec/impl/proof lines by supressing, e.g.,
 ghost statements

---
 Source/DafnyDriver/DafnyDriver.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 99d4938e..8046a7ac 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -147,7 +147,8 @@ namespace Microsoft.Dafny
         if (err != null) {
           exitValue = ExitValue.DAFNY_ERROR;
           printer.ErrorWriteLine(Console.Out, err);
-        } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
+        } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck
+            && DafnyOptions.O.DafnyVerify) {
           Dafny.Translator translator = new Dafny.Translator();
           Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
           if (CommandLineOptions.Clo.PrintFile != null)
-- 
cgit v1.2.3