From 717eaee0063074b804098d3cfd44a7a3f822b064 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 16 Feb 2010 05:07:46 +0000
Subject: Implemented block coalescing invoked right after type checking.
 Controlled by the option /coalesceBlocks (default is to perform the
 optimization).

---
 Source/BoogieDriver/BoogieDriver.ssc | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Source/BoogieDriver/BoogieDriver.ssc')

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index 035879ec..7b22d6fe 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -420,6 +420,11 @@ namespace Microsoft.Boogie
       // Eliminate dead variables
       Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
       
+      // Coalesce blocks
+      if (CommandLineOptions.Clo.CoalesceBlocks) {
+        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+      }
+      
       // Inline
       List<Declaration!>! TopLevelDeclarations = program.TopLevelDeclarations;
       if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
-- 
cgit v1.2.3