diff options
| author |  wuestholz <unknown> | 2013-12-09 09:48:11 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-12-09 09:48:11 +0100 |
| commit | 3de67fcd5ee66fa69c1b156fe67409812ee8a12c (patch) | |
| tree | a5d7964f49d45948258f50204548f41472ae3f61 /Source/DafnyDriver | |
| parent | 75aad652723efe9d0e41ee2e82f8123044b817a9 (diff) | |
Fix some things due to changes in Boogie (execution engine API, 'UnivBackPred2.smt2' no longer needed).
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 5 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.csproj | 3 |
2 files changed, 4 insertions, 4 deletions
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">
|