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

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index b5629b96..479816a6 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -40,6 +40,7 @@ namespace DafnyLanguage
         options.ApplyDefaultOptions();

 

         ExecutionEngine.printer = new DummyPrinter();

+        ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

       }

     }

 

@@ -230,8 +231,7 @@ namespace DafnyLanguage
 

       PipelineOutcome oc = BoogieResolveAndTypecheck(program);

       if (oc == PipelineOutcome.ResolvedAndTypeChecked) {

-        ExecutionEngine.EliminateDeadVariablesAndInline(program);

-        ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

+        ExecutionEngine.EliminateDeadVariablesAndInline(program);        

         return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId);

       }

       return oc;