updated answer files

og and linear creates some rearrangement of blocks

3 files changed, 116 insertions, 116 deletions

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index fe848aab..18359b2e 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -24,14 +24,7 @@ implementation Join(b: bool)
     y := 4;

     z := x + y;

     assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

-	goto Then, Else;

-

-  Then:

-    assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

-    assume b <==> true;

-    x := x + 1;

-    assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b;

-    goto join;

+    goto Then, Else;

 

   Else:

     assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

@@ -47,6 +40,13 @@ implementation Join(b: bool)
     assert GlobalFlag <==> true;

     assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7;

     return;

+

+  Then:

+    assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

+    assume b <==> true;

+    x := x + 1;

+    assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b;

+    goto join;

 }

 

 

@@ -72,17 +72,17 @@ implementation Loop()
     assume {:inferred} c == 0 && 0 <= i && i < 11;

     goto Then, Else;

 

+  Else:

+    assume {:inferred} c == 0 && 0 <= i && i < 11;

+    assume {:inferred} c == 0 && 0 <= i && i < 11;

+    return;

+

   Then:

     assume {:inferred} c == 0 && 0 <= i && i < 11;

     assume i < 10;

     i := i + 1;

     assume {:inferred} c == 0 && 1 <= i && i < 11;

     goto test;

-

-  Else:

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    return;

 }

 

 

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index bfe185e7..880e587b 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -18,18 +18,18 @@ implementation SimpleLoop()
     assume {:inferred} 0 <= i && i < 11;

     goto Then, Else;

 

+  Else:

+    assume {:inferred} 0 <= i && i < 11;

+    assume !(i < 10);

+    assume {:inferred} 0 <= i && i < 11;

+    return;

+

   Then:

     assume {:inferred} 0 <= i && i < 11;

     assume i < 10;

     i := i + 1;

     assume {:inferred} 1 <= i && i < 11;

     goto test;

-

-  Else:

-    assume {:inferred} 0 <= i && i < 11;

-    assume !(i < 10);

-    assume {:inferred} 0 <= i && i < 11;

-    return;

 }

 

 

@@ -53,18 +53,18 @@ implementation VariableBoundLoop(n: int)
     assume {:inferred} 0 <= i;

     goto Then, Else;

 

+  Else:

+    assume {:inferred} 0 <= i;

+    assume !(i < n);

+    assume {:inferred} 0 <= i;

+    return;

+

   Then:

     assume {:inferred} 0 <= i;

     assume i < n;

     i := i + 1;

     assume {:inferred} 1 <= i && 1 <= n;

     goto test;

-

-  Else:

-    assume {:inferred} 0 <= i;

-    assume !(i < n);

-    assume {:inferred} 0 <= i;

-    return;

 }

 

 

@@ -238,14 +238,14 @@ implementation p()
     assume {:inferred} true;

     goto B, C;

 

-  B:

+  C:

     assume {:inferred} true;

-    x := x * x;

     assume {:inferred} true;

     return;

 

-  C:

+  B:

     assume {:inferred} true;

+    x := x * x;

     assume {:inferred} true;

     return;

 }

@@ -272,6 +272,11 @@ implementation p()
     assume {:inferred} -1 <= x;

     goto B, E;

 

+  E:

+    assume {:inferred} true;

+    assume {:inferred} true;

+    return;

+

   B:

     assume {:inferred} -1 <= x;

     assume x < y;

@@ -289,11 +294,6 @@ implementation p()
     x := y;

     assume {:inferred} 0 <= x && 0 <= y;

     return;

-

-  E:

-    assume {:inferred} true;

-    assume {:inferred} true;

-    return;

 }

 

 

@@ -320,12 +320,6 @@ implementation p()
     assume {:inferred} x == 8;

     goto B, C;

 

-  B:

-    assume {:inferred} x == 8;

-    x := 9;

-    assume {:inferred} x == 9;

-    goto D;

-

   C:

     assume {:inferred} x == 8;

     x := 10;

@@ -336,6 +330,12 @@ implementation p()
     assume {:inferred} 9 <= x && x < 11;

     assume {:inferred} 9 <= x && x < 11;

     return;

+

+  B:

+    assume {:inferred} x == 8;

+    x := 9;

+    assume {:inferred} x == 9;

+    goto D;

 }

 

 

@@ -360,12 +360,6 @@ implementation p()
     assume {:inferred} true;

     goto B, C;

 

-  B:

-    assume {:inferred} true;

-    assume x <= 0;

-    assume {:inferred} x < 1;

-    goto D;

-

   C:

     assume {:inferred} true;

     assume y <= 0;

@@ -376,6 +370,12 @@ implementation p()
     assume {:inferred} true;

     assume {:inferred} true;

     return;

+

+  B:

+    assume {:inferred} true;

+    assume x <= 0;

+    assume {:inferred} x < 1;

+    goto D;

 }

 

 

diff --git a/Test/inline/Answer b/Test/inline/Answer
index aaaa138c..b6207739 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -355,11 +355,6 @@ implementation recursivetest()
   inline$recursive$0$anon0:

     goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

 

-  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$anon3_Else:

     assume {:partition} inline$recursive$0$x != 0;

     goto inline$recursive$1$Entry;

@@ -372,11 +367,6 @@ implementation recursivetest()
   inline$recursive$1$anon0:

     goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

 

-  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$anon3_Else:

     assume {:partition} inline$recursive$1$x != 0;

     goto inline$recursive$2$Entry;

@@ -389,17 +379,17 @@ implementation recursivetest()
   inline$recursive$2$anon0:

     goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

 

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

@@ -408,6 +398,11 @@ implementation recursivetest()
     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;

@@ -416,6 +411,11 @@ implementation recursivetest()
     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;

@@ -445,11 +445,6 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
   anon0:

     goto anon3_Then, anon3_Else;

 

-  anon3_Then:

-    assume {:partition} x == 0;

-    y := 1;

-    return;

-

   anon3_Else:

     assume {:partition} x != 0;

     goto inline$recursive$0$Entry;

@@ -462,11 +457,6 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
   inline$recursive$0$anon0:

     goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

 

-  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$anon3_Else:

     assume {:partition} inline$recursive$0$x != 0;

     goto inline$recursive$1$Entry;

@@ -479,11 +469,6 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
   inline$recursive$1$anon0:

     goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

 

-  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$anon3_Else:

     assume {:partition} inline$recursive$1$x != 0;

     goto inline$recursive$2$Entry;

@@ -496,17 +481,17 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
   inline$recursive$2$anon0:

     goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

 

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

@@ -515,6 +500,11 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     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;

@@ -523,6 +513,11 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     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;

@@ -530,6 +525,11 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
   anon3_Else$1:

     y := y + k;

     return;

+

+  anon3_Then:

+    assume {:partition} x == 0;

+    y := 1;

+    return;

 }

 

 

@@ -695,11 +695,6 @@ implementation main(x: int)
   inline$check$0$anon0:

     goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

 

-  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$anon4_Else:

     assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;

     inline$check$0$ret := false;

@@ -708,6 +703,11 @@ implementation main(x: int)
   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;

@@ -716,23 +716,23 @@ implementation main(x: int)
   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$anon5_Else:

-    assume {:partition} !inline$find$0$b;

-    goto inline$find$0$anon4_LoopHead;

+  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$anon3:

-    goto inline$find$0$Return;

-

   inline$find$0$Return:

     i := inline$find$0$ret;

     b := inline$find$0$found;

@@ -741,17 +741,17 @@ implementation main(x: int)
   anon0$1:

     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;

+

+  anon3_Then:

+    assume {:partition} b;

+    assert i > 0 && A[i] == x;

+    goto anon2;

 }

 

 

@@ -793,11 +793,6 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
   inline$check$0$anon0:

     goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

 

-  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$anon4_Else:

     assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;

     inline$check$0$ret := false;

@@ -806,6 +801,11 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
   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;

@@ -814,22 +814,22 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
   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;

 

-  anon5_Else:

-    assume {:partition} !b;

-    goto anon4_LoopHead;

+  anon3:

+    return;

 

   anon4_LoopDone:

     assume {:partition} size <= i;

     goto anon3;

-

-  anon3:

-    return;

 }

 

 

@@ -840,30 +840,30 @@ Execution trace:
     <console>(29,0): inline$find$0$anon0

     <console>(39,0): inline$find$0$anon4_LoopBody

     <console>(43,0): inline$check$0$Entry

-    <console>(59,0): inline$check$0$anon4_Else

-    <console>(64,0): inline$check$0$anon3

+    <console>(54,0): inline$check$0$anon4_Else

+    <console>(59,0): inline$check$0$anon3

     <console>(67,0): inline$check$0$Return

-<console>(102,4): Error BP5001: This assertion might not hold.

+<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>(54,0): inline$check$0$anon4_Then

+    <console>(62,0): inline$check$0$anon4_Then

     <console>(67,0): inline$check$0$Return

-    <console>(75,0): inline$find$0$anon5_Then

-    <console>(89,0): inline$find$0$anon3

+    <console>(79,0): inline$find$0$anon5_Then

+    <console>(85,0): inline$find$0$anon3

     <console>(92,0): inline$find$0$Return

     <console>(97,0): anon0$1

-    <console>(100,0): anon3_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>(40,0): inline$check$0$anon4_Else

-    <console>(45,0): inline$check$0$anon3

+    <console>(35,0): inline$check$0$anon4_Else

+    <console>(40,0): inline$check$0$anon3

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