From 0d06cb1b6a16fee1a789f3b1b674d59cfcd11d92 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sun, 11 Sep 2011 13:20:52 -0700
Subject: Dafny: generate a compiler error upon encountering an assume
 statement Dafny: don't compile programs unless all methods have been verified
 (or a forced compile is requested)

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

(limited to 'Source/DafnyDriver/DafnyDriver.cs')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index d8d0e0e0..1c6c1e77 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie
           switch (oc) {
             case PipelineOutcome.VerificationCompleted:
               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
-              if ((CommandLineOptions.Clo.Compile && allOk) || CommandLineOptions.Clo.ForceCompile)
+              if ((CommandLineOptions.Clo.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || CommandLineOptions.Clo.ForceCompile)
                 CompileDafnyProgram(dafnyProgram);
               break;
             case PipelineOutcome.Done:
-- 
cgit v1.2.3