Merging complete. Everything looks good *crosses fingers*

17 files changed, 730 insertions, 730 deletions

diff --git a/Test/inline/Elevator.asml b/Test/inline/Elevator.asml
index 02a58d10..e2d4bdf1 100644
--- a/Test/inline/Elevator.asml
+++ b/Test/inline/Elevator.asml
@@ -1,56 +1,56 @@
-var floors as Set of Integer

-var DoorsOpen as Set of Integer = {}

-var liftDoorOpen as Boolean = false

-var liftLevel as Integer = 1

-var moving as Boolean = false

-var headingTo as Integer = 0

-

-[Action]

-ButtonPress(i as Integer)

-  require i in floors

-  headingTo := i

-

-[Action]

-MoveUp()

-  require liftDoorOpen = false and liftLevel < headingTo

-  require not (liftLevel in DoorsOpen)

-  moving := true

-  liftLevel:= liftLevel + 1

-

-[Action]

-MoveDown()

-  //bug, should require that liftDoorOpen = false

-  require  liftLevel > headingTo and headingTo > 0

-  require not (liftLevel in DoorsOpen)

-  moving := true

-  liftLevel := liftLevel - 1

-

-[Action]  

-Stop()

-  require liftLevel = headingTo

-  moving := false

-  

-[Action]

-OpenLiftDoor()

-  require moving = false

-  liftDoorOpen := true

-  

-[Action]

-CloseLiftDoor()

-  liftDoorOpen := false  

-

-[Action]

-OpenFloorDoor(i as Integer)

-  require liftLevel = i 

-  DoorsOpen := DoorsOpen union {i}

-

-[Action]

-CloseFloorDoor(i as Integer)

-  DoorsOpen := DoorsOpen - {i}

-

-  

-Invariant ()

-  require not (liftDoorOpen = true and moving = true)

-  

-  

+var floors as Set of Integer
+var DoorsOpen as Set of Integer = {}
+var liftDoorOpen as Boolean = false
+var liftLevel as Integer = 1
+var moving as Boolean = false
+var headingTo as Integer = 0
+
+[Action]
+ButtonPress(i as Integer)
+  require i in floors
+  headingTo := i
+
+[Action]
+MoveUp()
+  require liftDoorOpen = false and liftLevel < headingTo
+  require not (liftLevel in DoorsOpen)
+  moving := true
+  liftLevel:= liftLevel + 1
+
+[Action]
+MoveDown()
+  //bug, should require that liftDoorOpen = false
+  require  liftLevel > headingTo and headingTo > 0
+  require not (liftLevel in DoorsOpen)
+  moving := true
+  liftLevel := liftLevel - 1
+
+[Action]  
+Stop()
+  require liftLevel = headingTo
+  moving := false
+  
+[Action]
+OpenLiftDoor()
+  require moving = false
+  liftDoorOpen := true
+  
+[Action]
+CloseLiftDoor()
+  liftDoorOpen := false  
+
+[Action]
+OpenFloorDoor(i as Integer)
+  require liftLevel = i 
+  DoorsOpen := DoorsOpen union {i}
+
+[Action]
+CloseFloorDoor(i as Integer)
+  DoorsOpen := DoorsOpen - {i}
+
+  
+Invariant ()
+  require not (liftDoorOpen = true and moving = true)
+  
+  
   
\ No newline at end of file
diff --git a/Test/inline/Elevator.bpl b/Test/inline/Elevator.bpl
index 2e146643..dc364ce2 100644
--- a/Test/inline/Elevator.bpl
+++ b/Test/inline/Elevator.bpl
@@ -1,156 +1,156 @@
-// 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

-var DoorsOpen: [int]bool;

-var liftDoorOpen: bool;

-var liftLevel: int;

-var moving: bool;

-var headingTo: int;

-

-procedure Main_Error()

-  modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;

-{

-  var i: int;

-

-  call Initialize();

-  while (true)

-    invariant !(liftDoorOpen && moving);

-  {

-    if (*) {

-      havoc i;  call ButtonPress(i);

-    } else if (*) {

-      call MoveUp();

-    } else if (*) {

-      call MoveDown_Error();

-    } else if (*) {

-      call Stop();

-    } else if (*) {

-      call OpenLiftDoor();

-    } else if (*) {

-      call CloseLiftDoor();

-    } else if (*) {

-      havoc i;  call OpenFloorDoor(i);

-    } else {

-      havoc i;  call CloseFloorDoor(i);

-    }

-  }

-}

-

-procedure Main_Correct()

-  modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;

-{

-  var i: int;

-

-  call Initialize();

-  while (true)

-    invariant !(liftDoorOpen && moving);

-  {

-    if (*) {

-      havoc i;  call ButtonPress(i);

-    } else if (*) {

-      call MoveUp();

-    } else if (*) {

-      call MoveDown_Correct();

-    } else if (*) {

-      call Stop();

-    } else if (*) {

-      call OpenLiftDoor();

-    } else if (*) {

-      call CloseLiftDoor();

-    } else if (*) {

-      havoc i;  call OpenFloorDoor(i);

-    } else {

-      havoc i;  call CloseFloorDoor(i);

-    }

-  }

-}

-

-procedure {:inline 1} Initialize()

-  modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;

-{

-  DoorsOpen := EmptySet;

-  liftDoorOpen := false;

-  liftLevel := 1;

-  moving := false;

-  headingTo := 0;

-}

-

-procedure {:inline 1} ButtonPress(i: int)

-  modifies headingTo;

-{

-  assume floors[i];

-  headingTo := i;

-}

-

-procedure {:inline 1} MoveUp()

-  modifies moving, liftLevel;

-{

-  assume !liftDoorOpen && liftLevel < headingTo;

-  assume !DoorsOpen[liftLevel];

-  moving := true;

-  liftLevel:= liftLevel + 1;

-}

-

-procedure {:inline 1} MoveDown_Error()

-  modifies moving, liftLevel;

-{

-  //bug, should require that liftDoorOpen = false

-  // assume !liftDoorOpen;

-  assume liftLevel > headingTo && headingTo > 0;

-  assume !DoorsOpen[liftLevel];

-  moving := true;

-  liftLevel := liftLevel - 1;

-}

-

-procedure {:inline 1} MoveDown_Correct()

-  modifies moving, liftLevel;

-{

-  assume !liftDoorOpen;

-  assume liftLevel > headingTo && headingTo > 0;

-  assume !DoorsOpen[liftLevel];

-  moving := true;

-  liftLevel := liftLevel - 1;

-}

-

-procedure {:inline 1} Stop()

-  modifies moving;

-{

-  assume liftLevel == headingTo;

-  moving := false;

-}

-  

-procedure {:inline 1} OpenLiftDoor()

-  modifies liftDoorOpen;

-{

-  assume !moving;

-  liftDoorOpen := true;

-}

-  

-procedure {:inline 1} CloseLiftDoor()

-  modifies liftDoorOpen;

-{

-  liftDoorOpen := false;

-}

-

-procedure {:inline 1} OpenFloorDoor(i: int)

-  modifies DoorsOpen;

-{

-  assume liftLevel == i;

-  DoorsOpen[i] := true;  // DoorsOpen := DoorsOpen union {i};

-}

-

-procedure {:inline 1} CloseFloorDoor(i: int)

-  modifies DoorsOpen;

-{

-  DoorsOpen[i] := false;  // DoorsOpen := DoorsOpen - {i}

-}

-

-// ---------------------------------------------------------------

-

-const EmptySet: [int]bool;

-axiom (forall o: int :: { EmptySet[o] } !EmptySet[o]);

-

-// ---------------------------------------------------------------

+// 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
+var DoorsOpen: [int]bool;
+var liftDoorOpen: bool;
+var liftLevel: int;
+var moving: bool;
+var headingTo: int;
+
+procedure Main_Error()
+  modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
+{
+  var i: int;
+
+  call Initialize();
+  while (true)
+    invariant !(liftDoorOpen && moving);
+  {
+    if (*) {
+      havoc i;  call ButtonPress(i);
+    } else if (*) {
+      call MoveUp();
+    } else if (*) {
+      call MoveDown_Error();
+    } else if (*) {
+      call Stop();
+    } else if (*) {
+      call OpenLiftDoor();
+    } else if (*) {
+      call CloseLiftDoor();
+    } else if (*) {
+      havoc i;  call OpenFloorDoor(i);
+    } else {
+      havoc i;  call CloseFloorDoor(i);
+    }
+  }
+}
+
+procedure Main_Correct()
+  modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
+{
+  var i: int;
+
+  call Initialize();
+  while (true)
+    invariant !(liftDoorOpen && moving);
+  {
+    if (*) {
+      havoc i;  call ButtonPress(i);
+    } else if (*) {
+      call MoveUp();
+    } else if (*) {
+      call MoveDown_Correct();
+    } else if (*) {
+      call Stop();
+    } else if (*) {
+      call OpenLiftDoor();
+    } else if (*) {
+      call CloseLiftDoor();
+    } else if (*) {
+      havoc i;  call OpenFloorDoor(i);
+    } else {
+      havoc i;  call CloseFloorDoor(i);
+    }
+  }
+}
+
+procedure {:inline 1} Initialize()
+  modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
+{
+  DoorsOpen := EmptySet;
+  liftDoorOpen := false;
+  liftLevel := 1;
+  moving := false;
+  headingTo := 0;
+}
+
+procedure {:inline 1} ButtonPress(i: int)
+  modifies headingTo;
+{
+  assume floors[i];
+  headingTo := i;
+}
+
+procedure {:inline 1} MoveUp()
+  modifies moving, liftLevel;
+{
+  assume !liftDoorOpen && liftLevel < headingTo;
+  assume !DoorsOpen[liftLevel];
+  moving := true;
+  liftLevel:= liftLevel + 1;
+}
+
+procedure {:inline 1} MoveDown_Error()
+  modifies moving, liftLevel;
+{
+  //bug, should require that liftDoorOpen = false
+  // assume !liftDoorOpen;
+  assume liftLevel > headingTo && headingTo > 0;
+  assume !DoorsOpen[liftLevel];
+  moving := true;
+  liftLevel := liftLevel - 1;
+}
+
+procedure {:inline 1} MoveDown_Correct()
+  modifies moving, liftLevel;
+{
+  assume !liftDoorOpen;
+  assume liftLevel > headingTo && headingTo > 0;
+  assume !DoorsOpen[liftLevel];
+  moving := true;
+  liftLevel := liftLevel - 1;
+}
+
+procedure {:inline 1} Stop()
+  modifies moving;
+{
+  assume liftLevel == headingTo;
+  moving := false;
+}
+  
+procedure {:inline 1} OpenLiftDoor()
+  modifies liftDoorOpen;
+{
+  assume !moving;
+  liftDoorOpen := true;
+}
+  
+procedure {:inline 1} CloseLiftDoor()
+  modifies liftDoorOpen;
+{
+  liftDoorOpen := false;
+}
+
+procedure {:inline 1} OpenFloorDoor(i: int)
+  modifies DoorsOpen;
+{
+  assume liftLevel == i;
+  DoorsOpen[i] := true;  // DoorsOpen := DoorsOpen union {i};
+}
+
+procedure {:inline 1} CloseFloorDoor(i: int)
+  modifies DoorsOpen;
+{
+  DoorsOpen[i] := false;  // DoorsOpen := DoorsOpen - {i}
+}
+
+// ---------------------------------------------------------------
+
+const EmptySet: [int]bool;
+axiom (forall o: int :: { EmptySet[o] } !EmptySet[o]);
+
+// ---------------------------------------------------------------
diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl
index 74b20913..52901480 100644
--- a/Test/inline/InliningAndLoops.bpl
+++ b/Test/inline/InliningAndLoops.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure foo(N: int)

-  requires N == 2;

-{

-  var n, sum, recent: int;

-  n, sum := 0, 0;

-  while (n < N)

-  {

-    call recent := bar();

-    sum, n := sum + recent, n + 1;

-  }

-  if (n == 2) {

-    assert sum == recent + recent;  // no reason to believe this always to be true

-  }

-}

-

-procedure {:inline 1} bar() returns (r: int)

-{

-  var x: int;

-  r := x;

-}

+// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(N: int)
+  requires N == 2;
+{
+  var n, sum, recent: int;
+  n, sum := 0, 0;
+  while (n < N)
+  {
+    call recent := bar();
+    sum, n := sum + recent, n + 1;
+  }
+  if (n == 2) {
+    assert sum == recent + recent;  // no reason to believe this always to be true
+  }
+}
+
+procedure {:inline 1} bar() returns (r: int)
+{
+  var x: int;
+  r := x;
+}
diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl
index 0b4ebeb6..185b518d 100644
--- a/Test/inline/codeexpr.bpl
+++ b/Test/inline/codeexpr.bpl
@@ -1,62 +1,62 @@
-// RUN: %boogie "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-var g: bool;

-

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

-{

-  l := g;

-}

-

-procedure {:inline 1} baz() returns (l: bool)

-{

-  call l := bar();

-}

-

-procedure A1() 

-modifies g;

-{

-    g := true;

-    assert |{ var l: bool; A: call l := bar(); return l; }|;

-    assert (exists p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);

-    assert (forall p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);

-}

-

-procedure A2() 

-{

-    assert |{ var l: bool; A: assume g; call l := bar(); return l; }|;

-    assert g ==> |{ var l: bool; A: call l := bar(); return l; }|;

-    assert (exists p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);

-    assert (forall p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);

-}

-

-procedure A3() 

-{

-    assume |{ var l: bool; A: call l := bar(); return l; }|;

-    assert |{ var l: bool; A: call l := bar(); return l; }|;

-}

-

-procedure A4()

-modifies g;

-{

-    g := true;

-    assert |{ var l: bool; A: call l := bar(); return !l; }|;

-}

-

-procedure A5() 

-modifies g;

-{

-    var m: bool;

-

-    g := true;

-    m := |{ var l: bool; A: call l := bar(); return l; }|;

-    assert m;

-}

-

-procedure A6() 

-modifies g;

-{

-    g := true;

-    assert |{ var l: bool; A: call l := baz(); return l; }|;

-    assert (exists p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);

-    assert (forall p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g: bool;
+
+procedure {:inline 1} bar() returns (l: bool) 
+{
+  l := g;
+}
+
+procedure {:inline 1} baz() returns (l: bool)
+{
+  call l := bar();
+}
+
+procedure A1() 
+modifies g;
+{
+    g := true;
+    assert |{ var l: bool; A: call l := bar(); return l; }|;
+    assert (exists p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);
+    assert (forall p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);
+}
+
+procedure A2() 
+{
+    assert |{ var l: bool; A: assume g; call l := bar(); return l; }|;
+    assert g ==> |{ var l: bool; A: call l := bar(); return l; }|;
+    assert (exists p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);
+    assert (forall p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);
+}
+
+procedure A3() 
+{
+    assume |{ var l: bool; A: call l := bar(); return l; }|;
+    assert |{ var l: bool; A: call l := bar(); return l; }|;
+}
+
+procedure A4()
+modifies g;
+{
+    g := true;
+    assert |{ var l: bool; A: call l := bar(); return !l; }|;
+}
+
+procedure A5() 
+modifies g;
+{
+    var m: bool;
+
+    g := true;
+    m := |{ var l: bool; A: call l := bar(); return l; }|;
+    assert m;
+}
+
+procedure A6() 
+modifies g;
+{
+    g := true;
+    assert |{ var l: bool; A: call l := baz(); return l; }|;
+    assert (exists p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);
+    assert (forall p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);
+}
diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl
index 9883ce83..18eaef33 100644
--- a/Test/inline/expansion2.bpl
+++ b/Test/inline/expansion2.bpl
@@ -1,19 +1,19 @@
-// 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)

-  { x + 1 }

-

-axiom (forall z:int :: z>12 ==> xxgz(z));

-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;

-}

-

+// 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)
+  { x + 1 }
+
+axiom (forall z:int :: z>12 ==> xxgz(z));
+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/expansion3.bpl b/Test/inline/expansion3.bpl
index bfb8b0fa..a6cbb411 100644
--- a/Test/inline/expansion3.bpl
+++ b/Test/inline/expansion3.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

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

- { foo3(x,y) }

-

-axiom foo3(1,false);

-

-procedure baz1()

-  requires foo3(2,false);

-{

-  assume foo3(1,true);

-}

-

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:inline true} foo3(x:int, y:bool) returns(bool)
+ { foo3(x,y) }
+
+axiom foo3(1,false);
+
+procedure baz1()
+  requires foo3(2,false);
+{
+  assume foo3(1,true);
+}
+
diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl
index 1c1ff51c..cfd0672d 100644
--- a/Test/inline/expansion4.bpl
+++ b/Test/inline/expansion4.bpl
@@ -1,11 +1,11 @@
-// RUN: %boogie "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-function foo(x:int) : int

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

-

-procedure bar()

-{

-  assert foo(0) == 1;

-  assert foo(1) == 3;

-  assert foo(2) == 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 }
+
+procedure bar()
+{
+  assert foo(0) == 1;
+  assert foo(1) == 3;
+  assert foo(2) == 5;
+}
diff --git a/Test/inline/fundef.bpl b/Test/inline/fundef.bpl
index 9c5b2cfd..1d2dd50d 100644
--- a/Test/inline/fundef.bpl
+++ b/Test/inline/fundef.bpl
@@ -1,8 +1,8 @@
-// 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)

-  { x > 0 }

-function foo3(x:int) returns(bool)

-  { x > 0 }

+// 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)
+  { x > 0 }
+function foo3(x:int) returns(bool)
+  { x > 0 }
diff --git a/Test/inline/fundef2.bpl b/Test/inline/fundef2.bpl
index 39453453..9e0f9fab 100644
--- a/Test/inline/fundef2.bpl
+++ b/Test/inline/fundef2.bpl
@@ -1,9 +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

-}

+// 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
+}
diff --git a/Test/inline/polyInline.bpl b/Test/inline/polyInline.bpl
index ed404867..709b8b41 100644
--- a/Test/inline/polyInline.bpl
+++ b/Test/inline/polyInline.bpl
@@ -1,43 +1,43 @@
-// 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;

-

-function empty<alpha>() returns (alpha);

-

-function eqC<alpha>(x:alpha) returns (bool) { x == C }

-function giveEmpty<alpha>() returns (alpha) { empty() }

-

-function {:inline true} eqC2<alpha>(x:alpha) returns (bool) { x == C }

-function {:inline true} giveEmpty2<alpha>() returns (alpha) { empty() }

-

-function eqC3<alpha>(x:alpha) returns (bool);

-axiom {:inline true} (forall<alpha> x:alpha :: eqC3(x) == (x == C));

-

-function giveEmpty3<alpha>() returns (alpha);

-axiom {:inline true} (forall<alpha> :: giveEmpty3():alpha == empty());

-

-procedure P() {

-  assert eqC(C);

-  assert eqC2(C);

-  assert eqC3(C);

-  assert eqC2(D);  // should not be provable

-}

-

-procedure Q() {

-  assert giveEmpty() == empty();

-  assert giveEmpty() == empty():int;

-  assert giveEmpty():bool == empty();

-

-  assert giveEmpty2() == empty();

-  assert giveEmpty2() == empty():int;

-  assert giveEmpty2():bool == empty();

-

-  assert giveEmpty3() == empty();

-  assert giveEmpty3() == empty():int;

-  assert giveEmpty3():bool == empty();

-

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

-}

+// 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;
+
+function empty<alpha>() returns (alpha);
+
+function eqC<alpha>(x:alpha) returns (bool) { x == C }
+function giveEmpty<alpha>() returns (alpha) { empty() }
+
+function {:inline true} eqC2<alpha>(x:alpha) returns (bool) { x == C }
+function {:inline true} giveEmpty2<alpha>() returns (alpha) { empty() }
+
+function eqC3<alpha>(x:alpha) returns (bool);
+axiom {:inline true} (forall<alpha> x:alpha :: eqC3(x) == (x == C));
+
+function giveEmpty3<alpha>() returns (alpha);
+axiom {:inline true} (forall<alpha> :: giveEmpty3():alpha == empty());
+
+procedure P() {
+  assert eqC(C);
+  assert eqC2(C);
+  assert eqC3(C);
+  assert eqC2(D);  // should not be provable
+}
+
+procedure Q() {
+  assert giveEmpty() == empty();
+  assert giveEmpty() == empty():int;
+  assert giveEmpty():bool == empty();
+
+  assert giveEmpty2() == empty();
+  assert giveEmpty2() == empty():int;
+  assert giveEmpty2():bool == empty();
+
+  assert giveEmpty3() == empty();
+  assert giveEmpty3() == empty():int;
+  assert giveEmpty3():bool == empty();
+
+  assert giveEmpty3() == C;     // should not be provable
+}
diff --git a/Test/inline/test0.bpl b/Test/inline/test0.bpl
index 6a2d9640..52006767 100644
--- a/Test/inline/test0.bpl
+++ b/Test/inline/test0.bpl
@@ -1,50 +1,50 @@
-// RUN: %boogie "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-// inlined functions

-

-function Twice(x: int) returns (int)

-{

-  x + x

-}

-

-function {:inline} Double(x: int) returns (int)

-{

-  3 * x - x

-}

-

-function f(int) returns (int);

-function g(int) returns (int);

-function h(int) returns (int);

-function k(int) returns (int);

-axiom (forall x: int :: Twice(x) == f(x));  // here, Twice(x) and f(x) are both triggers

-axiom (forall x: int :: Double(x) == g(x));  // since Double is inlined, the trigger here is just g(x)

-axiom (forall x: int :: { f(x) } f(x) < h(x) );

-axiom (forall x: int :: { g(x) } g(x) < k(x) );

-

-procedure P(a: int, b: int, c: int)

-{

-  // The following is provable, because Twice triggers its definition and the resulting f(a)

-  // triggers the relation to h(a).

-  assert Twice(a) < h(a);

-  if (*) {

-    // The following is NOT provable, because Double is inlined and thus no g(b) term is ever

-    // created

-    assert Double(b) < k(b);  // error

-  } else {

-    // The following IS provable, because the explicit g(c) will cause both of the necessary

-    // quantifiers to trigger

-    assert g(c) == 2*c;

-    assert Double(c) < k(c);

-  }

-}

-

-// nullary functions

-

-function Five() returns (int) { 5 }

-

-function {:inline} Eight() returns (e: int) { 8 }

-

-procedure Q()

-{

-  assert 8 * Five() == 5 * Eight();

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// inlined functions
+
+function Twice(x: int) returns (int)
+{
+  x + x
+}
+
+function {:inline} Double(x: int) returns (int)
+{
+  3 * x - x
+}
+
+function f(int) returns (int);
+function g(int) returns (int);
+function h(int) returns (int);
+function k(int) returns (int);
+axiom (forall x: int :: Twice(x) == f(x));  // here, Twice(x) and f(x) are both triggers
+axiom (forall x: int :: Double(x) == g(x));  // since Double is inlined, the trigger here is just g(x)
+axiom (forall x: int :: { f(x) } f(x) < h(x) );
+axiom (forall x: int :: { g(x) } g(x) < k(x) );
+
+procedure P(a: int, b: int, c: int)
+{
+  // The following is provable, because Twice triggers its definition and the resulting f(a)
+  // triggers the relation to h(a).
+  assert Twice(a) < h(a);
+  if (*) {
+    // The following is NOT provable, because Double is inlined and thus no g(b) term is ever
+    // created
+    assert Double(b) < k(b);  // error
+  } else {
+    // The following IS provable, because the explicit g(c) will cause both of the necessary
+    // quantifiers to trigger
+    assert g(c) == 2*c;
+    assert Double(c) < k(c);
+  }
+}
+
+// nullary functions
+
+function Five() returns (int) { 5 }
+
+function {:inline} Eight() returns (e: int) { 8 }
+
+procedure Q()
+{
+  assert 8 * Five() == 5 * Eight();
+}
diff --git a/Test/inline/test1.bpl b/Test/inline/test1.bpl
index 11ce6b4f..f9166965 100644
--- a/Test/inline/test1.bpl
+++ b/Test/inline/test1.bpl
@@ -1,47 +1,47 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-procedure Main()

-{

-

-	var x:int;

-	var y:int;

-

-	x := 1;

-	y := 0;

-

-	call x := inc(x, 5);

-	call y := incdec(x, 2);

-

-	assert(x - 1 == y);	

-

-}

-

-procedure {:inline 1} incdec(x:int, y:int) returns (z:int)

-	ensures z == x + 1 - y;

-{

-	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;

-{

-	y := x;

-	y := x + i;

-	return;

-	

-}

-

-procedure {:inline 1} dec(x:int, i:int) returns (y:int)

-	ensures y == x - i;

-{

-	y := x;

-	y := x - i;

-	return;

-	

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure Main()
+{
+
+	var x:int;
+	var y:int;
+
+	x := 1;
+	y := 0;
+
+	call x := inc(x, 5);
+	call y := incdec(x, 2);
+
+	assert(x - 1 == y);	
+
+}
+
+procedure {:inline 1} incdec(x:int, y:int) returns (z:int)
+	ensures z == x + 1 - y;
+{
+	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;
+{
+	y := x;
+	y := x + i;
+	return;
+	
+}
+
+procedure {:inline 1} dec(x:int, i:int) returns (y:int)
+	ensures y == x - i;
+{
+	y := x;
+	y := x - i;
+	return;
+	
 }
\ No newline at end of file
diff --git a/Test/inline/test2.bpl b/Test/inline/test2.bpl
index 981d7604..6c16d342 100644
--- a/Test/inline/test2.bpl
+++ b/Test/inline/test2.bpl
@@ -1,33 +1,33 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-var glb:int;

-

-procedure calculate()

-modifies glb;

-{

-	var x:int;

-	var y:int;

-	

-	y := 5;

-

-	call x := increase(y);

-	

-	return;

-}

-

-

-procedure {:inline 1} increase (i:int) returns (k:int)

-modifies glb;

-{

-	var j:int;

-	

-	j := i;

-	j := j + 1;

-	

-	glb := glb + j;

-

-	k := j;

-

-	return;

-}

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var glb:int;
+
+procedure calculate()
+modifies glb;
+{
+	var x:int;
+	var y:int;
+	
+	y := 5;
+
+	call x := increase(y);
+	
+	return;
+}
+
+
+procedure {:inline 1} increase (i:int) returns (k:int)
+modifies glb;
+{
+	var j:int;
+	
+	j := i;
+	j := j + 1;
+	
+	glb := glb + j;
+
+	k := j;
+
+	return;
+}
diff --git a/Test/inline/test3.bpl b/Test/inline/test3.bpl
index 2f8b1749..1af4485a 100644
--- a/Test/inline/test3.bpl
+++ b/Test/inline/test3.bpl
@@ -1,30 +1,30 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-var glb:int;

-

-procedure recursivetest()

-modifies glb;

-{

-	glb := 5;

-	call glb := recursive(glb);

-

-	return;

-

-}

-

-procedure {:inline 3} recursive(x:int) returns (y:int) 

-{

-

-	var k: int;	

-

-	if(x == 0) {

-		y := 1;

-		return;

-	}

-

-	call k := recursive(x-1);

-	y := y + k;

-	return;

-

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var glb:int;
+
+procedure recursivetest()
+modifies glb;
+{
+	glb := 5;
+	call glb := recursive(glb);
+
+	return;
+
+}
+
+procedure {:inline 3} recursive(x:int) returns (y:int) 
+{
+
+	var k: int;	
+
+	if(x == 0) {
+		y := 1;
+		return;
+	}
+
+	call k := recursive(x-1);
+	y := y + k;
+	return;
+
 }
\ No newline at end of file
diff --git a/Test/inline/test4.bpl b/Test/inline/test4.bpl
index 7743c498..2a646b58 100644
--- a/Test/inline/test4.bpl
+++ b/Test/inline/test4.bpl
@@ -1,55 +1,55 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-procedure main(x:int)

-{

-	var A:[int]int;

-	var i:int;

-	var b:bool;

-	var size:int;

-	

-	call i,b := find(A, size, x);

-

-	if(b) {

-		assert(i > 0 && A[i] == x);

-	}

-

-	return;

-}

-

-procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)

-{

-	var i:int;

-	var b:bool;

-

-	ret := -1;

-	b := false;

-	found := b;

-	i := 0;

-

-	while(i < size) {

-		call b := check(A, i, x);

-		if(b) {

-		      ret := i;

-		      found := b;

-		      break;

-		}

-	

-	}

-

-	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;

-{

-	if(A[i] == c) {

-		ret := true;

-	} else {

-	       ret := false;

-	}

-	return;

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure main(x:int)
+{
+	var A:[int]int;
+	var i:int;
+	var b:bool;
+	var size:int;
+	
+	call i,b := find(A, size, x);
+
+	if(b) {
+		assert(i > 0 && A[i] == x);
+	}
+
+	return;
+}
+
+procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
+{
+	var i:int;
+	var b:bool;
+
+	ret := -1;
+	b := false;
+	found := b;
+	i := 0;
+
+	while(i < size) {
+		call b := check(A, i, x);
+		if(b) {
+		      ret := i;
+		      found := b;
+		      break;
+		}
+	
+	}
+
+	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;
+{
+	if(A[i] == c) {
+		ret := true;
+	} else {
+	       ret := false;
+	}
+	return;
 }
\ No newline at end of file
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl
index d7a80737..a0a25faf 100644
--- a/Test/inline/test5.bpl
+++ b/Test/inline/test5.bpl
@@ -1,81 +1,81 @@
-// RUN: %boogie "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

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

-

-procedure {:inline 2} foo()

-  modifies x;

-{

-  x := x + 1;

-}

-

-var x:int;

-

-procedure  bar()

-  modifies x;

-{

-  x := 3;

-  call foo();

-  assert x == 4;

-  call foo();

-  assert x == 5;

-}

-

-// -------------------------------------------------

-

-var Mem : [int]int;

-

-procedure {:inline 1} P(x:int)

-  modifies Mem;

-{

-  Mem[x] := 1;

-}

-

-procedure mainA()

-  modifies Mem;

-{

-  Mem[1] := 0;

-  call P(0);

-  call P(1);

-  assert Mem[1] == 0;  // error

-}

-

-procedure mainB()

-  modifies Mem;

-{

-  Mem[1] := 0;

-  call P(0);

-  call P(1);

-  assert Mem[1] == 1;  // good

-}

-

-procedure mainC()

-  modifies Mem;

-{

-  Mem[1] := 0;

-  call P(0);

-  call P(1);

-  assert Mem[1] == 1;  // good

-}

-

-// -------------------------------------------------

-

-type ref;

-var xyz: ref;

-

-procedure xyzA();

-  modifies xyz;

-  ensures old(xyz) == xyz;

-

-procedure {:inline 1} xyzB()

-  modifies xyz;

-{

-  call xyzA();

-}

-

-procedure xyzMain()

-  modifies xyz;

-{

-  call xyzA();

-  assert old(xyz) == xyz;

-  call xyzB();

-}

+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// test a case, where the inlined proc comes before the caller
+
+procedure {:inline 2} foo()
+  modifies x;
+{
+  x := x + 1;
+}
+
+var x:int;
+
+procedure  bar()
+  modifies x;
+{
+  x := 3;
+  call foo();
+  assert x == 4;
+  call foo();
+  assert x == 5;
+}
+
+// -------------------------------------------------
+
+var Mem : [int]int;
+
+procedure {:inline 1} P(x:int)
+  modifies Mem;
+{
+  Mem[x] := 1;
+}
+
+procedure mainA()
+  modifies Mem;
+{
+  Mem[1] := 0;
+  call P(0);
+  call P(1);
+  assert Mem[1] == 0;  // error
+}
+
+procedure mainB()
+  modifies Mem;
+{
+  Mem[1] := 0;
+  call P(0);
+  call P(1);
+  assert Mem[1] == 1;  // good
+}
+
+procedure mainC()
+  modifies Mem;
+{
+  Mem[1] := 0;
+  call P(0);
+  call P(1);
+  assert Mem[1] == 1;  // good
+}
+
+// -------------------------------------------------
+
+type ref;
+var xyz: ref;
+
+procedure xyzA();
+  modifies xyz;
+  ensures old(xyz) == xyz;
+
+procedure {:inline 1} xyzB()
+  modifies xyz;
+{
+  call xyzA();
+}
+
+procedure xyzMain()
+  modifies xyz;
+{
+  call xyzA();
+  assert old(xyz) == xyz;
+  call xyzB();
+}
diff --git a/Test/inline/test6.bpl b/Test/inline/test6.bpl
index d2e034fc..386c8d94 100644
--- a/Test/inline/test6.bpl
+++ b/Test/inline/test6.bpl
@@ -1,39 +1,39 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure {:inline 2} foo()

-  modifies x;

-{

-  x := x + 1;

-  call foo();

-}

-

-procedure {:inline 2} foo1()

-  modifies x;

-{

-  x := x + 1;

-  call foo2();

-}

-

-procedure {:inline 2} foo2()

-  modifies x;

-{

-  x := x + 1;

-  call foo3();

-}

-

-procedure {:inline 2} foo3()

-  modifies x;

-{

-  x := x + 1;

-  call foo1();

-}

-

-var x:int;

-

-procedure  bar()

-  modifies x;

-{

-  call foo();

-  call foo1();

-}

-

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure {:inline 2} foo()
+  modifies x;
+{
+  x := x + 1;
+  call foo();
+}
+
+procedure {:inline 2} foo1()
+  modifies x;
+{
+  x := x + 1;
+  call foo2();
+}
+
+procedure {:inline 2} foo2()
+  modifies x;
+{
+  x := x + 1;
+  call foo3();
+}
+
+procedure {:inline 2} foo3()
+  modifies x;
+{
+  x := x + 1;
+  call foo1();
+}
+
+var x:int;
+
+procedure  bar()
+  modifies x;
+{
+  call foo();
+  call foo1();
+}
+