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

5 files changed, 9 insertions, 11 deletions

diff --git a/Binaries/PrepareDafnyZip.bat b/Binaries/PrepareDafnyZip.bat
index 29330621..e2521112 100644
--- a/Binaries/PrepareDafnyZip.bat
+++ b/Binaries/PrepareDafnyZip.bat
@@ -22,7 +22,6 @@ for %%f in (
   Model.dll                           Model.pdb
   ParserHelper.dll                    ParserHelper.pdb
   Provers.SMTLib.dll                  Provers.SMTLib.pdb
-  UnivBackPred2.smt2
   VCExpr.dll                          VCExpr.pdb
   VCGeneration.dll                    VCGeneration.pdb
   DafnyLanguageService.vsix
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index a2b5aa0b..b5414ba3 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -187,7 +187,10 @@ namespace Microsoft.Dafny
           return oc;

 

         case PipelineOutcome.ResolvedAndTypeChecked:

-          ExecutionEngine.EliminateDeadVariablesAndInline(program);

+          ExecutionEngine.EliminateDeadVariables(program);

+          ExecutionEngine.CollectModSets(program);

+          ExecutionEngine.CoalesceBlocks(program);

+          ExecutionEngine.Inline(program);

           return ExecutionEngine.InferAndVerify(program, stats);

 

         default:

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index 912fd38e..631b0194 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -178,9 +178,6 @@
     <None Include="app.config" />

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <PropertyGroup>

-    <PreBuildEvent>copy /y "$(SolutionDir)"..\..\boogie\Binaries\UnivBackPred2.smt2 "$(TargetDir)"</PreBuildEvent>

-  </PropertyGroup>

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it.

        Other similar extension points exist, see Microsoft.Common.targets.

   <Target Name="BeforeBuild">

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;

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 47a3516c..d29da5d2 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -163,9 +163,6 @@
     <Content Include="DafnyPrelude.bpl">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

-    <Content Include="UnivBackPred2.smt2">

-      <IncludeInVSIX>true</IncludeInVSIX>

-    </Content>

     <Content Include="DafnyRuntime.cs">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

@@ -189,8 +186,7 @@
   <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />

   <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />

   <PropertyGroup>

-    <PreBuildEvent>copy /y "..\..\boogie\Binaries\UnivBackPred2.smt2" "$(ProjectDir)"

-copy /y "..\Binaries\DafnyPrelude.bpl" "$(ProjectDir)"

+    <PreBuildEvent>copy /y "..\Binaries\DafnyPrelude.bpl" "$(ProjectDir)"

 copy /y "..\Binaries\DafnyRuntime.cs" "$(ProjectDir)"</PreBuildEvent>

   </PropertyGroup>

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it.