Implemented block coalescing invoked right after type checking.

Controlled by the option /coalesceBlocks (default is to perform the optimization).

1 files changed, 5 insertions, 3 deletions

diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index 4f04999c..199cb6f2 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -8,14 +8,16 @@ procedure p()
 {

   A:

     assume -1 <= x;

-    goto B;

+    goto B, E;

   B:

     assume x < y;

-    goto C;

+    goto C, E;

   C:

     x := x*x;

-    goto D;

+    goto D, E;

   D:

     x := y;

     return;

+  E:

+    return;

 }