Fix some things due to changes in Boogie (execution engine API, 'UnivBackPred2.smt2' no longer needed).

1 files changed, 4 insertions, 1 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 168e69b5..c92caf4e 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -251,7 +251,10 @@ namespace DafnyLanguage
 

       PipelineOutcome oc = BoogieResolveAndTypecheck(program);

       if (oc == PipelineOutcome.ResolvedAndTypeChecked) {

-        ExecutionEngine.EliminateDeadVariablesAndInline(program);        

+        ExecutionEngine.EliminateDeadVariables(program);

+        ExecutionEngine.CollectModSets(program);

+        ExecutionEngine.CoalesceBlocks(program);

+        ExecutionEngine.Inline(program);  

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

       }

       return oc;