updated answer files

og and linear creates some rearrangement of blocks

1 files changed, 32 insertions, 32 deletions

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;

 }