Enable Linear inequality lit tests.

1 files changed, 133 insertions, 0 deletions

diff --git a/Test/aitest1/ineq.bpl.expect b/Test/aitest1/ineq.bpl.expect
new file mode 100644
index 00000000..d6c36bdd
--- /dev/null
+++ b/Test/aitest1/ineq.bpl.expect
@@ -0,0 +1,133 @@
+procedure SimpleLoop();
+
+
+
+implementation SimpleLoop()
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 0;
+    assume {:inferred} i == 0;
+    goto test;
+
+  test:  // cut point
+    assume {:inferred} 0 <= i && i < 11;
+    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;
+}
+
+
+
+procedure VariableBoundLoop(n: int);
+
+
+
+implementation VariableBoundLoop(n: int)
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 0;
+    assume {:inferred} i == 0;
+    goto test;
+
+  test:  // cut point
+    assume {:inferred} 0 <= i;
+    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;
+}
+
+
+
+procedure Foo();
+
+
+
+implementation Foo()
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+procedure FooToo();
+
+
+
+implementation FooToo()
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 5;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume {:inferred} i == 465;
+    return;
+}
+
+
+
+procedure FooTooStepByStep();
+
+
+
+implementation FooTooStepByStep()
+{
+  var i: int;
+
+  L0:
+    assume {:inferred} true;
+    i := 5;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume {:inferred} i == 465;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors