summaryrefslogtreecommitdiff
path: root/Source/DafnyDriver/DafnyDriver.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/DafnyDriver/DafnyDriver.cs')
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs5
1 files changed, 4 insertions, 1 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: