From 5df8661c279d98990c2852f559d8b67fa9b0c92e Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 10 Jul 2013 18:21:14 -0700
Subject: Did some refactoring of the interaction with the Boogie execution
 engine.

---
 Source/DafnyDriver/DafnyDriver.cs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 43aa6971..81662b5d 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -163,7 +163,8 @@ namespace Microsoft.Dafny
       Contract.Ensures(0 <= Contract.ValueAtReturn(out stats).InconclusiveCount && 0 <= Contract.ValueAtReturn(out stats).TimeoutCount);
 
       stats = new PipelineStatistics();
-      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName);
+      LinearTypechecker ltc;
+      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc);
       switch (oc) {
         case PipelineOutcome.Done:
           return oc;
@@ -180,7 +181,7 @@ namespace Microsoft.Dafny
             fileNames.Add(bplFileName);
             Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true);
             if (reparsedProgram != null) {
-              ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName);
+              ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc);
             }
           }
           return oc;
@@ -190,7 +191,7 @@ namespace Microsoft.Dafny
           return ExecutionEngine.InferAndVerify(program, stats);
 
         default:
-          Contract.Assert(false);throw new cce.UnreachableException();  // unexpected outcome
+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome
       }
     }
 
-- 
cgit v1.2.3