Did some refactoring of the interaction with the Boogie execution engine.

1 files changed, 4 insertions, 3 deletions

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

       }

     }