Enabled the inline lit tests. In order to support expansion2.bpl

we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.

33 files changed, 1648 insertions, 61 deletions

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 6a3f6ba7..88e3ed5f 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1,14 +1,14 @@
 -------------------- test0.bpl --------------------

-test0.bpl(30,5): Error BP5001: This assertion might not hold.

+test0.bpl(32,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    test0.bpl(26,3): anon0

-    test0.bpl(30,5): anon3_Then

+    test0.bpl(28,3): anon0

+    test0.bpl(32,5): anon3_Then

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- codeexpr.bpl --------------------

-codeexpr.bpl(40,5): Error BP5001: This assertion might not hold.

+codeexpr.bpl(42,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    codeexpr.bpl(39,7): anon0

+    codeexpr.bpl(41,7): anon0

 

 Boogie program verifier finished with 5 verified, 1 error

 -------------------- test1.bpl --------------------

@@ -1455,12 +1455,12 @@ implementation bar()
 

 Boogie program verifier finished with 5 verified, 0 errors

 -------------------- test5.bpl --------------------

-test5.bpl(37,3): Error BP5001: This assertion might not hold.

+test5.bpl(39,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    test5.bpl(34,10): anon0

-    test5.bpl(28,10): inline$P$0$anon0

-    test5.bpl(28,10): inline$P$1$anon0

-    test5.bpl(34,10): anon0$2

+    test5.bpl(36,10): anon0

+    test5.bpl(30,10): inline$P$0$anon0

+    test5.bpl(30,10): inline$P$1$anon0

+    test5.bpl(36,10): anon0$2

 

 Boogie program verifier finished with 4 verified, 1 error

 -------------------- expansion3.bpl --------------------

@@ -1473,33 +1473,33 @@ Boogie program verifier finished with 1 verified, 0 errors
 

 Boogie program verifier finished with 1 verified, 0 errors

 -------------------- Elevator.bpl --------------------

-Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

+Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.

 Execution trace:

-    Elevator.bpl(15,3): anon0

-    Elevator.bpl(15,3): anon0$1

-    Elevator.bpl(16,3): anon10_LoopHead

-    Elevator.bpl(19,5): anon10_LoopBody

-    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

-    Elevator.bpl(24,7): anon13_Then$1

+    Elevator.bpl(18,3): anon0

+    Elevator.bpl(18,3): anon0$1

+    Elevator.bpl(19,3): anon10_LoopHead

+    Elevator.bpl(22,5): anon10_LoopBody

+    Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0

+    Elevator.bpl(27,7): anon13_Then$1

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- Elevator.bpl with empty blocks --------------------

-Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

+Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.

 Execution trace:

-    Elevator.bpl(15,3): anon0

-    Elevator.bpl(68,23): inline$Initialize$0$Entry

-    Elevator.bpl(71,13): inline$Initialize$0$anon0

-    Elevator.bpl(68,23): inline$Initialize$0$Return

-    Elevator.bpl(15,3): anon0$1

-    Elevator.bpl(16,3): anon10_LoopHead

-    Elevator.bpl(19,5): anon10_LoopBody

-    Elevator.bpl(19,5): anon11_Else

-    Elevator.bpl(19,5): anon12_Else

-    Elevator.bpl(24,7): anon13_Then

-    Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry

-    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

-    Elevator.bpl(94,23): inline$MoveDown_Error$0$Return

-    Elevator.bpl(24,7): anon13_Then$1

+    Elevator.bpl(18,3): anon0

+    Elevator.bpl(71,23): inline$Initialize$0$Entry

+    Elevator.bpl(74,13): inline$Initialize$0$anon0

+    Elevator.bpl(71,23): inline$Initialize$0$Return

+    Elevator.bpl(18,3): anon0$1

+    Elevator.bpl(19,3): anon10_LoopHead

+    Elevator.bpl(22,5): anon10_LoopBody

+    Elevator.bpl(22,5): anon11_Else

+    Elevator.bpl(22,5): anon12_Else

+    Elevator.bpl(27,7): anon13_Then

+    Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry

+    Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0

+    Elevator.bpl(97,23): inline$MoveDown_Error$0$Return

+    Elevator.bpl(27,7): anon13_Then$1

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- expansion2.bpl --------------------

@@ -1525,46 +1525,46 @@ function foo3(x: int) : bool;
 axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

 

 Boogie program verifier finished with 0 verified, 0 errors

-fundef2.bpl(6,3): Error BP5001: This assertion might not hold.

+fundef2.bpl(8,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    fundef2.bpl(5,3): anon0

+    fundef2.bpl(7,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 -------------------- polyInline.bpl --------------------

-polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(23,3): Error BP5001: This assertion might not hold.

+polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int

+polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int

+polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int

+polyInline.bpl(26,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(20,3): anon0

-polyInline.bpl(39,3): Error BP5001: This assertion might not hold.

+    polyInline.bpl(23,3): anon0

+polyInline.bpl(42,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(27,3): anon0

+    polyInline.bpl(30,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

-polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(23,3): Error BP5001: This assertion might not hold.

+polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int

+polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int

+polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int

+polyInline.bpl(26,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(20,3): anon0

-polyInline.bpl(39,3): Error BP5001: This assertion might not hold.

+    polyInline.bpl(23,3): anon0

+polyInline.bpl(42,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(27,3): anon0

+    polyInline.bpl(30,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

 -------------------- InliningAndLoops.bpl --------------------

-InliningAndLoops.bpl(12,5): Error BP5001: This assertion might not hold.

+InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    InliningAndLoops.bpl(5,10): anon0#3

-    InliningAndLoops.bpl(6,3): anon4_LoopHead#3

-    InliningAndLoops.bpl(8,5): anon4_LoopBody#3

-    InliningAndLoops.bpl(8,5): anon4_LoopBody$1#3

-    InliningAndLoops.bpl(6,3): anon4_LoopHead#2

-    InliningAndLoops.bpl(8,5): anon4_LoopBody#2

-    InliningAndLoops.bpl(8,5): anon4_LoopBody$1#2

-    InliningAndLoops.bpl(6,3): anon4_LoopHead#1

-    InliningAndLoops.bpl(6,3): anon4_LoopDone#3

-    InliningAndLoops.bpl(12,5): anon5_Then#3

+    InliningAndLoops.bpl(7,10): anon0#3

+    InliningAndLoops.bpl(8,3): anon4_LoopHead#3

+    InliningAndLoops.bpl(10,5): anon4_LoopBody#3

+    InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3

+    InliningAndLoops.bpl(8,3): anon4_LoopHead#2

+    InliningAndLoops.bpl(10,5): anon4_LoopBody#2

+    InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2

+    InliningAndLoops.bpl(8,3): anon4_LoopHead#1

+    InliningAndLoops.bpl(8,3): anon4_LoopDone#3

+    InliningAndLoops.bpl(14,5): anon5_Then#3

 

 Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/inline/Elevator.bpl b/Test/inline/Elevator.bpl
index 4ee1e997..7a6b8128 100644
--- a/Test/inline/Elevator.bpl
+++ b/Test/inline/Elevator.bpl
@@ -1,3 +1,6 @@
+// RUN: %boogie %s > %t

+// RUN: %boogie -removeEmptyBlocks:0 %s >> %t

+// RUN: %diff %s.expect %t

 // A Boogie version of Elevator.asml (see Boogie/Test/inline/Elevator.asml)

 

 var floors: [int]bool;  // set of integer

diff --git a/Test/inline/Elevator.bpl.expect b/Test/inline/Elevator.bpl.expect
new file mode 100644
index 00000000..87141605
--- /dev/null
+++ b/Test/inline/Elevator.bpl.expect
@@ -0,0 +1,28 @@
+Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+    Elevator.bpl(18,3): anon0
+    Elevator.bpl(18,3): anon0$1
+    Elevator.bpl(19,3): anon10_LoopHead
+    Elevator.bpl(22,5): anon10_LoopBody
+    Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0
+    Elevator.bpl(27,7): anon13_Then$1
+
+Boogie program verifier finished with 1 verified, 1 error
+Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+    Elevator.bpl(18,3): anon0
+    Elevator.bpl(71,23): inline$Initialize$0$Entry
+    Elevator.bpl(74,13): inline$Initialize$0$anon0
+    Elevator.bpl(71,23): inline$Initialize$0$Return
+    Elevator.bpl(18,3): anon0$1
+    Elevator.bpl(19,3): anon10_LoopHead
+    Elevator.bpl(22,5): anon10_LoopBody
+    Elevator.bpl(22,5): anon11_Else
+    Elevator.bpl(22,5): anon12_Else
+    Elevator.bpl(27,7): anon13_Then
+    Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry
+    Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0
+    Elevator.bpl(97,23): inline$MoveDown_Error$0$Return
+    Elevator.bpl(27,7): anon13_Then$1
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl
index 970591a5..a22fd18c 100644
--- a/Test/inline/InliningAndLoops.bpl
+++ b/Test/inline/InliningAndLoops.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling %s > %t

+// RUN: %diff %s.expect %t

 procedure foo(N: int)

   requires N == 2;

 {

diff --git a/Test/inline/InliningAndLoops.bpl.expect b/Test/inline/InliningAndLoops.bpl.expect
new file mode 100644
index 00000000..b5c38542
--- /dev/null
+++ b/Test/inline/InliningAndLoops.bpl.expect
@@ -0,0 +1,14 @@
+InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    InliningAndLoops.bpl(7,10): anon0#3
+    InliningAndLoops.bpl(8,3): anon4_LoopHead#3
+    InliningAndLoops.bpl(10,5): anon4_LoopBody#3
+    InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3
+    InliningAndLoops.bpl(8,3): anon4_LoopHead#2
+    InliningAndLoops.bpl(10,5): anon4_LoopBody#2
+    InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2
+    InliningAndLoops.bpl(8,3): anon4_LoopHead#1
+    InliningAndLoops.bpl(8,3): anon4_LoopDone#3
+    InliningAndLoops.bpl(14,5): anon5_Then#3
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl
index 67728ea5..f9cef515 100644
--- a/Test/inline/codeexpr.bpl
+++ b/Test/inline/codeexpr.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 var g: bool;

 

 procedure {:inline 1} bar() returns (l: bool) 

diff --git a/Test/inline/codeexpr.bpl.expect b/Test/inline/codeexpr.bpl.expect
new file mode 100644
index 00000000..b42164c8
--- /dev/null
+++ b/Test/inline/codeexpr.bpl.expect
@@ -0,0 +1,5 @@
+codeexpr.bpl(42,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    codeexpr.bpl(41,7): anon0
+
+Boogie program verifier finished with 5 verified, 1 error
diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl
index b6ed19ed..da13d50f 100644
--- a/Test/inline/expansion2.bpl
+++ b/Test/inline/expansion2.bpl
@@ -1,3 +1,6 @@
+// RUN: %boogie -proverLog:%T/expand2.sx %s > %t

+// RUN: %diff %s.expect %t

+// RUN: %OutputCheck --file-to-check=%T/expand2.sx %s

 function {:inline true} xxgz(x:int) returns(bool)

  { x > 0 }

 function {:inline true} xxf1(x:int,y:bool) returns(int)

@@ -8,7 +11,9 @@ axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);
 

 procedure foo()

 {

+  // CHECK-NOT-L: xxgz

   assert xxgz(12);

+  // CHECK-NOT-L: xxf1

   assert xxf1(3,true) == 4;

 }

 

diff --git a/Test/inline/expansion2.bpl.expect b/Test/inline/expansion2.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/inline/expansion2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl
index 2b1f0caa..8d95166c 100644
--- a/Test/inline/expansion3.bpl
+++ b/Test/inline/expansion3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 function {:inline true} foo3(x:int, y:bool) returns(bool)

  { foo3(x,y) }

 

diff --git a/Test/inline/expansion3.bpl.expect b/Test/inline/expansion3.bpl.expect
new file mode 100644
index 00000000..072e091a
--- /dev/null
+++ b/Test/inline/expansion3.bpl.expect
@@ -0,0 +1,5 @@
+*** detected expansion loop on foo3
+*** detected expansion loop on foo3
+*** detected expansion loop on foo3
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl
index be11a391..c8bbe923 100644
--- a/Test/inline/expansion4.bpl
+++ b/Test/inline/expansion4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 function foo(x:int) : int

   { if x <= 0 then 1 else foo(x - 1) + 2 }

 

diff --git a/Test/inline/expansion4.bpl.expect b/Test/inline/expansion4.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/inline/expansion4.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/inline/fundef.bpl b/Test/inline/fundef.bpl
index 46ce65bd..a7298c9c 100644
--- a/Test/inline/fundef.bpl
+++ b/Test/inline/fundef.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -print:- -env:0 %s > %t

+// RUN: %diff %s.expect %t

 function {:inline true} foo(x:int) returns(bool)

   { x > 0 }

 function {:inline false} foo2(x:int) returns(bool)

diff --git a/Test/inline/fundef.bpl.expect b/Test/inline/fundef.bpl.expect
new file mode 100644
index 00000000..5adced6d
--- /dev/null
+++ b/Test/inline/fundef.bpl.expect
@@ -0,0 +1,15 @@
+
+function {:inline true} foo(x: int) : bool
+{
+  x > 0
+}
+
+function {:inline false} foo2(x: int) : bool;
+
+axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));
+
+function foo3(x: int) : bool;
+
+axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/inline/fundef2.bpl b/Test/inline/fundef2.bpl
index 2e005fcc..527d235d 100644
--- a/Test/inline/fundef2.bpl
+++ b/Test/inline/fundef2.bpl
@@ -1,7 +1,9 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 function {:inline true} foo(x:int) returns(bool)

   { x > 0 }

 

 procedure P() {

   assert foo(13);

   assert foo(-5);  // error

-}
\ No newline at end of file
+}

diff --git a/Test/inline/fundef2.bpl.expect b/Test/inline/fundef2.bpl.expect
new file mode 100644
index 00000000..f237e98a
--- /dev/null
+++ b/Test/inline/fundef2.bpl.expect
@@ -0,0 +1,5 @@
+fundef2.bpl(8,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    fundef2.bpl(7,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/inline/polyInline.bpl b/Test/inline/polyInline.bpl
index 320259bd..1f6ea200 100644
--- a/Test/inline/polyInline.bpl
+++ b/Test/inline/polyInline.bpl
@@ -1,3 +1,6 @@
+// RUN: %boogie /typeEncoding:predicates /logPrefix:p %s > %t

+// RUN: %boogie /typeEncoding:arguments /logPrefix:a %s >> %t

+// RUN: %diff %s.expect %t

 

 const C:int;

 const D:bool;

@@ -37,4 +40,4 @@ procedure Q() {
   assert giveEmpty3():bool == empty();

 

   assert giveEmpty3() == C;     // should not be provable

-}
\ No newline at end of file
+}

diff --git a/Test/inline/polyInline.bpl.expect b/Test/inline/polyInline.bpl.expect
new file mode 100644
index 00000000..e0fc093f
--- /dev/null
+++ b/Test/inline/polyInline.bpl.expect
@@ -0,0 +1,22 @@
+polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    polyInline.bpl(23,3): anon0
+polyInline.bpl(42,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    polyInline.bpl(30,3): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors
+polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    polyInline.bpl(23,3): anon0
+polyInline.bpl(42,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    polyInline.bpl(30,3): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors
diff --git a/Test/inline/test0.bpl b/Test/inline/test0.bpl
index 1b46f8c7..9a547d77 100644
--- a/Test/inline/test0.bpl
+++ b/Test/inline/test0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 // inlined functions

 

 function Twice(x: int) returns (int)

diff --git a/Test/inline/test0.bpl.expect b/Test/inline/test0.bpl.expect
new file mode 100644
index 00000000..46485036
--- /dev/null
+++ b/Test/inline/test0.bpl.expect
@@ -0,0 +1,6 @@
+test0.bpl(32,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    test0.bpl(28,3): anon0
+    test0.bpl(32,5): anon3_Then
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/inline/test1.bpl b/Test/inline/test1.bpl
index db847b25..1414978b 100644
--- a/Test/inline/test1.bpl
+++ b/Test/inline/test1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

+// RUN: %diff %s.expect %t

 

 procedure Main()

 {

diff --git a/Test/inline/test1.bpl.expect b/Test/inline/test1.bpl.expect
new file mode 100644
index 00000000..7b796e50
--- /dev/null
+++ b/Test/inline/test1.bpl.expect
@@ -0,0 +1,191 @@
+
+procedure Main();
+
+
+
+implementation Main()
+{
+  var x: int;
+  var y: int;
+
+  anon0:
+    x := 1;
+    y := 0;
+    call x := inc(x, 5);
+    call y := incdec(x, 2);
+    assert x - 1 == y;
+    return;
+}
+
+
+
+procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
+  ensures z == x + 1 - y;
+
+
+
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
+{
+
+  anon0:
+    z := x;
+    z := x + 1;
+    call z := dec(z, y);
+    return;
+}
+
+
+
+procedure {:inline 1} inc(x: int, i: int) returns (y: int);
+  ensures y == x + i;
+
+
+
+implementation {:inline 1} inc(x: int, i: int) returns (y: int)
+{
+
+  anon0:
+    y := x;
+    y := x + i;
+    return;
+}
+
+
+
+procedure {:inline 1} dec(x: int, i: int) returns (y: int);
+  ensures y == x - i;
+
+
+
+implementation {:inline 1} dec(x: int, i: int) returns (y: int)
+{
+
+  anon0:
+    y := x;
+    y := x - i;
+    return;
+}
+
+
+after inlining procedure calls
+procedure Main();
+
+
+implementation Main()
+{
+  var x: int;
+  var y: int;
+  var inline$inc$0$x: int;
+  var inline$inc$0$i: int;
+  var inline$inc$0$y: int;
+  var inline$incdec$0$x: int;
+  var inline$incdec$0$y: int;
+  var inline$incdec$0$z: int;
+  var inline$dec$0$x: int;
+  var inline$dec$0$i: int;
+  var inline$dec$0$y: int;
+
+  anon0:
+    x := 1;
+    y := 0;
+    goto inline$inc$0$Entry;
+
+  inline$inc$0$Entry:
+    inline$inc$0$x := x;
+    inline$inc$0$i := 5;
+    havoc inline$inc$0$y;
+    goto inline$inc$0$anon0;
+
+  inline$inc$0$anon0:
+    inline$inc$0$y := inline$inc$0$x;
+    inline$inc$0$y := inline$inc$0$x + inline$inc$0$i;
+    goto inline$inc$0$Return;
+
+  inline$inc$0$Return:
+    assert inline$inc$0$y == inline$inc$0$x + inline$inc$0$i;
+    x := inline$inc$0$y;
+    goto anon0$1;
+
+  anon0$1:
+    goto inline$incdec$0$Entry;
+
+  inline$incdec$0$Entry:
+    inline$incdec$0$x := x;
+    inline$incdec$0$y := 2;
+    havoc inline$incdec$0$z;
+    goto inline$incdec$0$anon0;
+
+  inline$incdec$0$anon0:
+    inline$incdec$0$z := inline$incdec$0$x;
+    inline$incdec$0$z := inline$incdec$0$x + 1;
+    goto inline$dec$0$Entry;
+
+  inline$dec$0$Entry:
+    inline$dec$0$x := inline$incdec$0$z;
+    inline$dec$0$i := inline$incdec$0$y;
+    havoc inline$dec$0$y;
+    goto inline$dec$0$anon0;
+
+  inline$dec$0$anon0:
+    inline$dec$0$y := inline$dec$0$x;
+    inline$dec$0$y := inline$dec$0$x - inline$dec$0$i;
+    goto inline$dec$0$Return;
+
+  inline$dec$0$Return:
+    assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i;
+    inline$incdec$0$z := inline$dec$0$y;
+    goto inline$incdec$0$anon0$1;
+
+  inline$incdec$0$anon0$1:
+    goto inline$incdec$0$Return;
+
+  inline$incdec$0$Return:
+    assert inline$incdec$0$z == inline$incdec$0$x + 1 - inline$incdec$0$y;
+    y := inline$incdec$0$z;
+    goto anon0$2;
+
+  anon0$2:
+    assert x - 1 == y;
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
+  ensures z == x + 1 - y;
+
+
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
+{
+  var inline$dec$0$x: int;
+  var inline$dec$0$i: int;
+  var inline$dec$0$y: int;
+
+  anon0:
+    z := x;
+    z := x + 1;
+    goto inline$dec$0$Entry;
+
+  inline$dec$0$Entry:
+    inline$dec$0$x := z;
+    inline$dec$0$i := y;
+    havoc inline$dec$0$y;
+    goto inline$dec$0$anon0;
+
+  inline$dec$0$anon0:
+    inline$dec$0$y := inline$dec$0$x;
+    inline$dec$0$y := inline$dec$0$x - inline$dec$0$i;
+    goto inline$dec$0$Return;
+
+  inline$dec$0$Return:
+    assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i;
+    z := inline$dec$0$y;
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/inline/test2.bpl b/Test/inline/test2.bpl
index a45e86d5..7cafdf62 100644
--- a/Test/inline/test2.bpl
+++ b/Test/inline/test2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

+// RUN: %diff %s.expect %t

 

 var glb:int;

 

diff --git a/Test/inline/test2.bpl.expect b/Test/inline/test2.bpl.expect
new file mode 100644
index 00000000..14521adb
--- /dev/null
+++ b/Test/inline/test2.bpl.expect
@@ -0,0 +1,81 @@
+
+var glb: int;
+
+procedure calculate();
+  modifies glb;
+
+
+
+implementation calculate()
+{
+  var x: int;
+  var y: int;
+
+  anon0:
+    y := 5;
+    call x := increase(y);
+    return;
+}
+
+
+
+procedure {:inline 1} increase(i: int) returns (k: int);
+  modifies glb;
+
+
+
+implementation {:inline 1} increase(i: int) returns (k: int)
+{
+  var j: int;
+
+  anon0:
+    j := i;
+    j := j + 1;
+    glb := glb + j;
+    k := j;
+    return;
+}
+
+
+after inlining procedure calls
+procedure calculate();
+  modifies glb;
+
+
+implementation calculate()
+{
+  var x: int;
+  var y: int;
+  var inline$increase$0$j: int;
+  var inline$increase$0$i: int;
+  var inline$increase$0$k: int;
+  var inline$increase$0$glb: int;
+
+  anon0:
+    y := 5;
+    goto inline$increase$0$Entry;
+
+  inline$increase$0$Entry:
+    inline$increase$0$i := y;
+    havoc inline$increase$0$j, inline$increase$0$k;
+    inline$increase$0$glb := glb;
+    goto inline$increase$0$anon0;
+
+  inline$increase$0$anon0:
+    inline$increase$0$j := inline$increase$0$i;
+    inline$increase$0$j := inline$increase$0$j + 1;
+    glb := glb + inline$increase$0$j;
+    inline$increase$0$k := inline$increase$0$j;
+    goto inline$increase$0$Return;
+
+  inline$increase$0$Return:
+    x := inline$increase$0$k;
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/inline/test3.bpl b/Test/inline/test3.bpl
index f705e7b0..3db73413 100644
--- a/Test/inline/test3.bpl
+++ b/Test/inline/test3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

+// RUN: %diff %s.expect %t

 

 var glb:int;

 

diff --git a/Test/inline/test3.bpl.expect b/Test/inline/test3.bpl.expect
new file mode 100644
index 00000000..79545583
--- /dev/null
+++ b/Test/inline/test3.bpl.expect
@@ -0,0 +1,255 @@
+
+var glb: int;
+
+procedure recursivetest();
+  modifies glb;
+
+
+
+implementation recursivetest()
+{
+
+  anon0:
+    glb := 5;
+    call glb := recursive(glb);
+    return;
+}
+
+
+
+procedure {:inline 3} recursive(x: int) returns (y: int);
+
+
+
+implementation {:inline 3} recursive(x: int) returns (y: int)
+{
+  var k: int;
+
+  anon0:
+    goto anon3_Then, anon3_Else;
+
+  anon3_Then:
+    assume {:partition} x == 0;
+    y := 1;
+    return;
+
+  anon3_Else:
+    assume {:partition} x != 0;
+    goto anon2;
+
+  anon2:
+    call k := recursive(x - 1);
+    y := y + k;
+    return;
+}
+
+
+after inlining procedure calls
+procedure recursivetest();
+  modifies glb;
+
+
+implementation recursivetest()
+{
+  var inline$recursive$0$k: int;
+  var inline$recursive$0$x: int;
+  var inline$recursive$0$y: int;
+  var inline$recursive$1$k: int;
+  var inline$recursive$1$x: int;
+  var inline$recursive$1$y: int;
+  var inline$recursive$2$k: int;
+  var inline$recursive$2$x: int;
+  var inline$recursive$2$y: int;
+
+  anon0:
+    glb := 5;
+    goto inline$recursive$0$Entry;
+
+  inline$recursive$0$Entry:
+    inline$recursive$0$x := glb;
+    havoc inline$recursive$0$k, inline$recursive$0$y;
+    goto inline$recursive$0$anon0;
+
+  inline$recursive$0$anon0:
+    goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;
+
+  inline$recursive$0$anon3_Else:
+    assume {:partition} inline$recursive$0$x != 0;
+    goto inline$recursive$1$Entry;
+
+  inline$recursive$1$Entry:
+    inline$recursive$1$x := inline$recursive$0$x - 1;
+    havoc inline$recursive$1$k, inline$recursive$1$y;
+    goto inline$recursive$1$anon0;
+
+  inline$recursive$1$anon0:
+    goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;
+
+  inline$recursive$1$anon3_Else:
+    assume {:partition} inline$recursive$1$x != 0;
+    goto inline$recursive$2$Entry;
+
+  inline$recursive$2$Entry:
+    inline$recursive$2$x := inline$recursive$1$x - 1;
+    havoc inline$recursive$2$k, inline$recursive$2$y;
+    goto inline$recursive$2$anon0;
+
+  inline$recursive$2$anon0:
+    goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;
+
+  inline$recursive$2$anon3_Else:
+    assume {:partition} inline$recursive$2$x != 0;
+    call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
+    inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
+    goto inline$recursive$2$Return;
+
+  inline$recursive$2$anon3_Then:
+    assume {:partition} inline$recursive$2$x == 0;
+    inline$recursive$2$y := 1;
+    goto inline$recursive$2$Return;
+
+  inline$recursive$2$Return:
+    inline$recursive$1$k := inline$recursive$2$y;
+    goto inline$recursive$1$anon3_Else$1;
+
+  inline$recursive$1$anon3_Else$1:
+    inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
+    goto inline$recursive$1$Return;
+
+  inline$recursive$1$anon3_Then:
+    assume {:partition} inline$recursive$1$x == 0;
+    inline$recursive$1$y := 1;
+    goto inline$recursive$1$Return;
+
+  inline$recursive$1$Return:
+    inline$recursive$0$k := inline$recursive$1$y;
+    goto inline$recursive$0$anon3_Else$1;
+
+  inline$recursive$0$anon3_Else$1:
+    inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
+    goto inline$recursive$0$Return;
+
+  inline$recursive$0$anon3_Then:
+    assume {:partition} inline$recursive$0$x == 0;
+    inline$recursive$0$y := 1;
+    goto inline$recursive$0$Return;
+
+  inline$recursive$0$Return:
+    glb := inline$recursive$0$y;
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 3} recursive(x: int) returns (y: int);
+
+
+implementation {:inline 3} recursive(x: int) returns (y: int)
+{
+  var k: int;
+  var inline$recursive$0$k: int;
+  var inline$recursive$0$x: int;
+  var inline$recursive$0$y: int;
+  var inline$recursive$1$k: int;
+  var inline$recursive$1$x: int;
+  var inline$recursive$1$y: int;
+  var inline$recursive$2$k: int;
+  var inline$recursive$2$x: int;
+  var inline$recursive$2$y: int;
+
+  anon0:
+    goto anon3_Then, anon3_Else;
+
+  anon3_Else:
+    assume {:partition} x != 0;
+    goto inline$recursive$0$Entry;
+
+  inline$recursive$0$Entry:
+    inline$recursive$0$x := x - 1;
+    havoc inline$recursive$0$k, inline$recursive$0$y;
+    goto inline$recursive$0$anon0;
+
+  inline$recursive$0$anon0:
+    goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;
+
+  inline$recursive$0$anon3_Else:
+    assume {:partition} inline$recursive$0$x != 0;
+    goto inline$recursive$1$Entry;
+
+  inline$recursive$1$Entry:
+    inline$recursive$1$x := inline$recursive$0$x - 1;
+    havoc inline$recursive$1$k, inline$recursive$1$y;
+    goto inline$recursive$1$anon0;
+
+  inline$recursive$1$anon0:
+    goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;
+
+  inline$recursive$1$anon3_Else:
+    assume {:partition} inline$recursive$1$x != 0;
+    goto inline$recursive$2$Entry;
+
+  inline$recursive$2$Entry:
+    inline$recursive$2$x := inline$recursive$1$x - 1;
+    havoc inline$recursive$2$k, inline$recursive$2$y;
+    goto inline$recursive$2$anon0;
+
+  inline$recursive$2$anon0:
+    goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;
+
+  inline$recursive$2$anon3_Else:
+    assume {:partition} inline$recursive$2$x != 0;
+    call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
+    inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
+    goto inline$recursive$2$Return;
+
+  inline$recursive$2$anon3_Then:
+    assume {:partition} inline$recursive$2$x == 0;
+    inline$recursive$2$y := 1;
+    goto inline$recursive$2$Return;
+
+  inline$recursive$2$Return:
+    inline$recursive$1$k := inline$recursive$2$y;
+    goto inline$recursive$1$anon3_Else$1;
+
+  inline$recursive$1$anon3_Else$1:
+    inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
+    goto inline$recursive$1$Return;
+
+  inline$recursive$1$anon3_Then:
+    assume {:partition} inline$recursive$1$x == 0;
+    inline$recursive$1$y := 1;
+    goto inline$recursive$1$Return;
+
+  inline$recursive$1$Return:
+    inline$recursive$0$k := inline$recursive$1$y;
+    goto inline$recursive$0$anon3_Else$1;
+
+  inline$recursive$0$anon3_Else$1:
+    inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
+    goto inline$recursive$0$Return;
+
+  inline$recursive$0$anon3_Then:
+    assume {:partition} inline$recursive$0$x == 0;
+    inline$recursive$0$y := 1;
+    goto inline$recursive$0$Return;
+
+  inline$recursive$0$Return:
+    k := inline$recursive$0$y;
+    goto anon3_Else$1;
+
+  anon3_Else$1:
+    y := y + k;
+    return;
+
+  anon3_Then:
+    assume {:partition} x == 0;
+    y := 1;
+    return;
+}
+
+
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/inline/test4.bpl b/Test/inline/test4.bpl
index 4a740bbc..248dfc6e 100644
--- a/Test/inline/test4.bpl
+++ b/Test/inline/test4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

+// RUN: %diff %s.expect %t

 

 procedure main(x:int)

 {

diff --git a/Test/inline/test4.bpl.expect b/Test/inline/test4.bpl.expect
new file mode 100644
index 00000000..29f80858
--- /dev/null
+++ b/Test/inline/test4.bpl.expect
@@ -0,0 +1,332 @@
+
+procedure main(x: int);
+
+
+
+implementation main(x: int)
+{
+  var A: [int]int;
+  var i: int;
+  var b: bool;
+  var size: int;
+
+  anon0:
+    call i, b := find(A, size, x);
+    goto anon3_Then, anon3_Else;
+
+  anon3_Then:
+    assume {:partition} b;
+    assert i > 0 && A[i] == x;
+    goto anon2;
+
+  anon3_Else:
+    assume {:partition} !b;
+    goto anon2;
+
+  anon2:
+    return;
+}
+
+
+
+procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
+
+
+
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+{
+  var i: int;
+  var b: bool;
+
+  anon0:
+    ret := -1;
+    b := false;
+    found := b;
+    i := 0;
+    goto anon4_LoopHead;
+
+  anon4_LoopHead:
+    goto anon4_LoopDone, anon4_LoopBody;
+
+  anon4_LoopBody:
+    assume {:partition} i < size;
+    call b := check(A, i, x);
+    goto anon5_Then, anon5_Else;
+
+  anon5_Then:
+    assume {:partition} b;
+    ret := i;
+    found := b;
+    goto anon3;
+
+  anon5_Else:
+    assume {:partition} !b;
+    goto anon4_LoopHead;
+
+  anon4_LoopDone:
+    assume {:partition} size <= i;
+    goto anon3;
+
+  anon3:
+    return;
+}
+
+
+
+procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool);
+  requires i >= 0;
+  ensures old(A[i]) > c ==> ret == true;
+
+
+
+implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)
+{
+
+  anon0:
+    goto anon4_Then, anon4_Else;
+
+  anon4_Then:
+    assume {:partition} A[i] == c;
+    ret := true;
+    goto anon3;
+
+  anon4_Else:
+    assume {:partition} A[i] != c;
+    ret := false;
+    goto anon3;
+
+  anon3:
+    return;
+}
+
+
+after inlining procedure calls
+procedure main(x: int);
+
+
+implementation main(x: int)
+{
+  var A: [int]int;
+  var i: int;
+  var b: bool;
+  var size: int;
+  var inline$find$0$i: int;
+  var inline$find$0$b: bool;
+  var inline$find$0$A: [int]int;
+  var inline$find$0$size: int;
+  var inline$find$0$x: int;
+  var inline$find$0$ret: int;
+  var inline$find$0$found: bool;
+  var inline$check$0$A: [int]int;
+  var inline$check$0$i: int;
+  var inline$check$0$c: int;
+  var inline$check$0$ret: bool;
+
+  anon0:
+    goto inline$find$0$Entry;
+
+  inline$find$0$Entry:
+    inline$find$0$A := A;
+    inline$find$0$size := size;
+    inline$find$0$x := x;
+    havoc inline$find$0$i, inline$find$0$b, inline$find$0$ret, inline$find$0$found;
+    goto inline$find$0$anon0;
+
+  inline$find$0$anon0:
+    inline$find$0$ret := -1;
+    inline$find$0$b := false;
+    inline$find$0$found := inline$find$0$b;
+    inline$find$0$i := 0;
+    goto inline$find$0$anon4_LoopHead;
+
+  inline$find$0$anon4_LoopHead:
+    goto inline$find$0$anon4_LoopDone, inline$find$0$anon4_LoopBody;
+
+  inline$find$0$anon4_LoopBody:
+    assume {:partition} inline$find$0$i < inline$find$0$size;
+    goto inline$check$0$Entry;
+
+  inline$check$0$Entry:
+    inline$check$0$A := inline$find$0$A;
+    inline$check$0$i := inline$find$0$i;
+    inline$check$0$c := inline$find$0$x;
+    assert inline$check$0$i >= 0;
+    havoc inline$check$0$ret;
+    goto inline$check$0$anon0;
+
+  inline$check$0$anon0:
+    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;
+
+  inline$check$0$anon4_Else:
+    assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;
+    inline$check$0$ret := false;
+    goto inline$check$0$anon3;
+
+  inline$check$0$anon3:
+    goto inline$check$0$Return;
+
+  inline$check$0$anon4_Then:
+    assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c;
+    inline$check$0$ret := true;
+    goto inline$check$0$anon3;
+
+  inline$check$0$Return:
+    assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true);
+    inline$find$0$b := inline$check$0$ret;
+    goto inline$find$0$anon4_LoopBody$1;
+
+  inline$find$0$anon4_LoopBody$1:
+    goto inline$find$0$anon5_Then, inline$find$0$anon5_Else;
+
+  inline$find$0$anon5_Else:
+    assume {:partition} !inline$find$0$b;
+    goto inline$find$0$anon4_LoopHead;
+
+  inline$find$0$anon5_Then:
+    assume {:partition} inline$find$0$b;
+    inline$find$0$ret := inline$find$0$i;
+    inline$find$0$found := inline$find$0$b;
+    goto inline$find$0$anon3;
+
+  inline$find$0$anon3:
+    goto inline$find$0$Return;
+
+  inline$find$0$anon4_LoopDone:
+    assume {:partition} inline$find$0$size <= inline$find$0$i;
+    goto inline$find$0$anon3;
+
+  inline$find$0$Return:
+    i := inline$find$0$ret;
+    b := inline$find$0$found;
+    goto anon0$1;
+
+  anon0$1:
+    goto anon3_Then, anon3_Else;
+
+  anon3_Else:
+    assume {:partition} !b;
+    goto anon2;
+
+  anon2:
+    return;
+
+  anon3_Then:
+    assume {:partition} b;
+    assert i > 0 && A[i] == x;
+    goto anon2;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
+
+
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+{
+  var i: int;
+  var b: bool;
+  var inline$check$0$A: [int]int;
+  var inline$check$0$i: int;
+  var inline$check$0$c: int;
+  var inline$check$0$ret: bool;
+
+  anon0:
+    ret := -1;
+    b := false;
+    found := b;
+    i := 0;
+    goto anon4_LoopHead;
+
+  anon4_LoopHead:
+    goto anon4_LoopDone, anon4_LoopBody;
+
+  anon4_LoopBody:
+    assume {:partition} i < size;
+    goto inline$check$0$Entry;
+
+  inline$check$0$Entry:
+    inline$check$0$A := A;
+    inline$check$0$i := i;
+    inline$check$0$c := x;
+    assert inline$check$0$i >= 0;
+    havoc inline$check$0$ret;
+    goto inline$check$0$anon0;
+
+  inline$check$0$anon0:
+    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;
+
+  inline$check$0$anon4_Else:
+    assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;
+    inline$check$0$ret := false;
+    goto inline$check$0$anon3;
+
+  inline$check$0$anon3:
+    goto inline$check$0$Return;
+
+  inline$check$0$anon4_Then:
+    assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c;
+    inline$check$0$ret := true;
+    goto inline$check$0$anon3;
+
+  inline$check$0$Return:
+    assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true);
+    b := inline$check$0$ret;
+    goto anon4_LoopBody$1;
+
+  anon4_LoopBody$1:
+    goto anon5_Then, anon5_Else;
+
+  anon5_Else:
+    assume {:partition} !b;
+    goto anon4_LoopHead;
+
+  anon5_Then:
+    assume {:partition} b;
+    ret := i;
+    found := b;
+    goto anon3;
+
+  anon3:
+    return;
+
+  anon4_LoopDone:
+    assume {:partition} size <= i;
+    goto anon3;
+}
+
+
+<console>(70,4): Error BP5003: A postcondition might not hold on this return path.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+    <console>(19,0): anon0
+    <console>(29,0): inline$find$0$anon0
+    <console>(39,0): inline$find$0$anon4_LoopBody
+    <console>(43,0): inline$check$0$Entry
+    <console>(54,0): inline$check$0$anon4_Else
+    <console>(67,0): inline$check$0$Return
+<console>(109,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    <console>(19,0): anon0
+    <console>(29,0): inline$find$0$anon0
+    <console>(39,0): inline$find$0$anon4_LoopBody
+    <console>(43,0): inline$check$0$Entry
+    <console>(62,0): inline$check$0$anon4_Then
+    <console>(67,0): inline$check$0$Return
+    <console>(79,0): inline$find$0$anon5_Then
+    <console>(107,0): anon3_Then
+<console>(51,4): Error BP5003: A postcondition might not hold on this return path.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+    <console>(10,0): anon0
+    <console>(20,0): anon4_LoopBody
+    <console>(24,0): inline$check$0$Entry
+    <console>(35,0): inline$check$0$anon4_Else
+    <console>(48,0): inline$check$0$Return
+<console>(99,0): Error BP5003: A postcondition might not hold on this return path.
+<console>(78,2): Related location: This is the postcondition that might not hold.
+Execution trace:
+    <console>(85,0): anon0
+    <console>(93,0): anon4_Else
+    <console>(98,0): anon3
+
+Boogie program verifier finished with 0 verified, 4 errors
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl
index 6460232c..8e092261 100644
--- a/Test/inline/test5.bpl
+++ b/Test/inline/test5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 // test a case, where the inlined proc comes before the caller

 

 procedure {:inline 2} foo()

diff --git a/Test/inline/test5.bpl.expect b/Test/inline/test5.bpl.expect
new file mode 100644
index 00000000..cd0530dd
--- /dev/null
+++ b/Test/inline/test5.bpl.expect
@@ -0,0 +1,8 @@
+test5.bpl(39,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    test5.bpl(36,10): anon0
+    test5.bpl(30,10): inline$P$0$anon0
+    test5.bpl(30,10): inline$P$1$anon0
+    test5.bpl(36,10): anon0$2
+
+Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/inline/test6.bpl b/Test/inline/test6.bpl
index 394be89e..febf1aae 100644
--- a/Test/inline/test6.bpl
+++ b/Test/inline/test6.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

+// RUN: %diff %s.expect %t

 procedure {:inline 2} foo()

   modifies x;

 {

diff --git a/Test/inline/test6.bpl.expect b/Test/inline/test6.bpl.expect
new file mode 100644
index 00000000..240094e1
--- /dev/null
+++ b/Test/inline/test6.bpl.expect
@@ -0,0 +1,579 @@
+
+procedure {:inline 2} foo();
+  modifies x;
+
+
+
+implementation {:inline 2} foo()
+{
+
+  anon0:
+    x := x + 1;
+    call foo();
+    return;
+}
+
+
+
+procedure {:inline 2} foo1();
+  modifies x;
+
+
+
+implementation {:inline 2} foo1()
+{
+
+  anon0:
+    x := x + 1;
+    call foo2();
+    return;
+}
+
+
+
+procedure {:inline 2} foo2();
+  modifies x;
+
+
+
+implementation {:inline 2} foo2()
+{
+
+  anon0:
+    x := x + 1;
+    call foo3();
+    return;
+}
+
+
+
+procedure {:inline 2} foo3();
+  modifies x;
+
+
+
+implementation {:inline 2} foo3()
+{
+
+  anon0:
+    x := x + 1;
+    call foo1();
+    return;
+}
+
+
+
+var x: int;
+
+procedure bar();
+  modifies x;
+
+
+
+implementation bar()
+{
+
+  anon0:
+    call foo();
+    call foo1();
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo();
+  modifies x;
+
+
+implementation {:inline 2} foo()
+{
+  var inline$foo$0$x: int;
+  var inline$foo$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo$0$Entry;
+
+  inline$foo$0$Entry:
+    inline$foo$0$x := x;
+    goto inline$foo$0$anon0;
+
+  inline$foo$0$anon0:
+    x := x + 1;
+    goto inline$foo$1$Entry;
+
+  inline$foo$1$Entry:
+    inline$foo$1$x := x;
+    goto inline$foo$1$anon0;
+
+  inline$foo$1$anon0:
+    x := x + 1;
+    call foo();
+    goto inline$foo$1$Return;
+
+  inline$foo$1$Return:
+    goto inline$foo$0$anon0$1;
+
+  inline$foo$0$anon0$1:
+    goto inline$foo$0$Return;
+
+  inline$foo$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo1();
+  modifies x;
+
+
+implementation {:inline 2} foo1()
+{
+  var inline$foo2$0$x: int;
+  var inline$foo3$0$x: int;
+  var inline$foo1$0$x: int;
+  var inline$foo2$1$x: int;
+  var inline$foo3$1$x: int;
+  var inline$foo1$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    call foo2();
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$1$anon0$1;
+
+  inline$foo3$1$anon0$1:
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$1$anon0$1;
+
+  inline$foo2$1$anon0$1:
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo2();
+  modifies x;
+
+
+implementation {:inline 2} foo2()
+{
+  var inline$foo3$0$x: int;
+  var inline$foo1$0$x: int;
+  var inline$foo2$0$x: int;
+  var inline$foo3$1$x: int;
+  var inline$foo1$1$x: int;
+  var inline$foo2$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    call foo3();
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$1$anon0$1;
+
+  inline$foo1$1$anon0$1:
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$1$anon0$1;
+
+  inline$foo3$1$anon0$1:
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo3();
+  modifies x;
+
+
+implementation {:inline 2} foo3()
+{
+  var inline$foo1$0$x: int;
+  var inline$foo2$0$x: int;
+  var inline$foo3$0$x: int;
+  var inline$foo1$1$x: int;
+  var inline$foo2$1$x: int;
+  var inline$foo3$1$x: int;
+
+  anon0:
+    x := x + 1;
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    call foo1();
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$1$anon0$1;
+
+  inline$foo2$1$anon0$1:
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$1$anon0$1;
+
+  inline$foo1$1$anon0$1:
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    return;
+}
+
+
+after inlining procedure calls
+procedure bar();
+  modifies x;
+
+
+implementation bar()
+{
+  var inline$foo$0$x: int;
+  var inline$foo$1$x: int;
+  var inline$foo1$0$x: int;
+  var inline$foo2$0$x: int;
+  var inline$foo3$0$x: int;
+  var inline$foo1$1$x: int;
+  var inline$foo2$1$x: int;
+  var inline$foo3$1$x: int;
+
+  anon0:
+    goto inline$foo$0$Entry;
+
+  inline$foo$0$Entry:
+    inline$foo$0$x := x;
+    goto inline$foo$0$anon0;
+
+  inline$foo$0$anon0:
+    x := x + 1;
+    goto inline$foo$1$Entry;
+
+  inline$foo$1$Entry:
+    inline$foo$1$x := x;
+    goto inline$foo$1$anon0;
+
+  inline$foo$1$anon0:
+    x := x + 1;
+    call foo();
+    goto inline$foo$1$Return;
+
+  inline$foo$1$Return:
+    goto inline$foo$0$anon0$1;
+
+  inline$foo$0$anon0$1:
+    goto inline$foo$0$Return;
+
+  inline$foo$0$Return:
+    goto anon0$1;
+
+  anon0$1:
+    goto inline$foo1$0$Entry;
+
+  inline$foo1$0$Entry:
+    inline$foo1$0$x := x;
+    goto inline$foo1$0$anon0;
+
+  inline$foo1$0$anon0:
+    x := x + 1;
+    goto inline$foo2$0$Entry;
+
+  inline$foo2$0$Entry:
+    inline$foo2$0$x := x;
+    goto inline$foo2$0$anon0;
+
+  inline$foo2$0$anon0:
+    x := x + 1;
+    goto inline$foo3$0$Entry;
+
+  inline$foo3$0$Entry:
+    inline$foo3$0$x := x;
+    goto inline$foo3$0$anon0;
+
+  inline$foo3$0$anon0:
+    x := x + 1;
+    goto inline$foo1$1$Entry;
+
+  inline$foo1$1$Entry:
+    inline$foo1$1$x := x;
+    goto inline$foo1$1$anon0;
+
+  inline$foo1$1$anon0:
+    x := x + 1;
+    goto inline$foo2$1$Entry;
+
+  inline$foo2$1$Entry:
+    inline$foo2$1$x := x;
+    goto inline$foo2$1$anon0;
+
+  inline$foo2$1$anon0:
+    x := x + 1;
+    goto inline$foo3$1$Entry;
+
+  inline$foo3$1$Entry:
+    inline$foo3$1$x := x;
+    goto inline$foo3$1$anon0;
+
+  inline$foo3$1$anon0:
+    x := x + 1;
+    call foo1();
+    goto inline$foo3$1$Return;
+
+  inline$foo3$1$Return:
+    goto inline$foo2$1$anon0$1;
+
+  inline$foo2$1$anon0$1:
+    goto inline$foo2$1$Return;
+
+  inline$foo2$1$Return:
+    goto inline$foo1$1$anon0$1;
+
+  inline$foo1$1$anon0$1:
+    goto inline$foo1$1$Return;
+
+  inline$foo1$1$Return:
+    goto inline$foo3$0$anon0$1;
+
+  inline$foo3$0$anon0$1:
+    goto inline$foo3$0$Return;
+
+  inline$foo3$0$Return:
+    goto inline$foo2$0$anon0$1;
+
+  inline$foo2$0$anon0$1:
+    goto inline$foo2$0$Return;
+
+  inline$foo2$0$Return:
+    goto inline$foo1$0$anon0$1;
+
+  inline$foo1$0$anon0$1:
+    goto inline$foo1$0$Return;
+
+  inline$foo1$0$Return:
+    goto anon0$2;
+
+  anon0$2:
+    return;
+}
+
+
+
+Boogie program verifier finished with 5 verified, 0 errors