5 files changed, 145 insertions, 0 deletions
diff --git a/Test/aitest9/Output b/Test/aitest9/Output
new file mode 100644
index 00000000..dd10a8b3
--- /dev/null
+++ b/Test/aitest9/Output
@@ -0,0 +1,26 @@
+ 
+-------------------- VarMapFixPoint.bpl -------------------- 
+VarMapFixPoint.bpl(11,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+    VarMapFixPoint.bpl(5,3): start
+    VarMapFixPoint.bpl(10,3): LoopHead
+    VarMapFixPoint.bpl(14,3): LoopBody
+
+Boogie program verifier finished with 1 verified, 1 error
+ 
+-------------------- TestIntervals.bpl -------------------- 
+TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    TestIntervals.bpl(5,5): anon0
+    TestIntervals.bpl(6,3): anon9_LoopHead
+    TestIntervals.bpl(6,3): anon9_LoopDone
+    TestIntervals.bpl(11,5): anon2
+    TestIntervals.bpl(12,14): anon10_Then
+    TestIntervals.bpl(13,3): anon4
+    TestIntervals.bpl(13,14): anon11_Then
+    TestIntervals.bpl(14,3): anon6
+    TestIntervals.bpl(14,14): anon12_Then
+    TestIntervals.bpl(17,5): anon8
+    TestIntervals.bpl(21,3): Next
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl
new file mode 100644
index 00000000..b989e16c
--- /dev/null
+++ b/Test/aitest9/TestIntervals.bpl
@@ -0,0 +1,24 @@
+procedure P()
+{
+  var a: int, b: int, c: int;
+
+  a := 0;
+  while (*) {
+    a := a + 1;
+  }
+  // a in [0, infty]
+
+  b := 0;
+  if (*) { b := b + 1; }
+  if (*) { b := b + 1; }
+  if (*) { b := b + 1; }
+  // b in [0, 3]
+
+  c := a - b;
+  // c in [-3, infty]
+  goto Next;
+
+  Next:
+  assert -3 <= c;
+  assert c <= 0;  // error (there was once an error in the Intervals which thought this assertion to be true)
+}
diff --git a/Test/aitest9/VarMapFixpoint.bpl b/Test/aitest9/VarMapFixpoint.bpl
new file mode 100644
index 00000000..6b53467d
--- /dev/null
+++ b/Test/aitest9/VarMapFixpoint.bpl
@@ -0,0 +1,58 @@
+procedure main()
+{
+  var x: int, y: int, z: int;
+
+  start:
+    x := 2;
+    y := 6;
+    goto LoopHead;
+
+  LoopHead:
+    assert y < 10;  // error: the loop body sets y to an arbitrary value
+    goto LoopBody, LoopEnd;
+
+  LoopBody:
+    havoc y;
+    goto LoopHead;
+
+  LoopEnd:
+    return;
+}
+
+procedure SimpleWhile5() returns (returnValue: int)
+{
+  var i: int;
+
+  start:
+    returnValue := 1;
+    havoc i;
+    goto LoopHead;
+
+  LoopHead:
+    goto LoopBody, LoopEnd;
+
+  LoopBody:
+    // here, we would simply like to "assume 1 <= i", but the interval domain doesn't interpret
+    // assume commands, so we start a loop
+    i := 1;
+    goto IncLoopHead;
+
+  IncLoopHead:
+    goto IncI, IncDone;
+
+  IncI:
+    i := i + 1;
+    goto IncLoopHead;
+
+  IncDone:
+    // now we have 1 <= i
+    assert 1 <= i;
+
+    returnValue := returnValue * i;
+    i := i - 1;
+    goto LoopHead;
+
+  LoopEnd:
+    assert returnValue >= 1;
+    return;
+}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer
new file mode 100644
index 00000000..dd10a8b3
--- /dev/null
+++ b/Test/aitest9/answer
@@ -0,0 +1,26 @@
+ 
+-------------------- VarMapFixPoint.bpl -------------------- 
+VarMapFixPoint.bpl(11,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+    VarMapFixPoint.bpl(5,3): start
+    VarMapFixPoint.bpl(10,3): LoopHead
+    VarMapFixPoint.bpl(14,3): LoopBody
+
+Boogie program verifier finished with 1 verified, 1 error
+ 
+-------------------- TestIntervals.bpl -------------------- 
+TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    TestIntervals.bpl(5,5): anon0
+    TestIntervals.bpl(6,3): anon9_LoopHead
+    TestIntervals.bpl(6,3): anon9_LoopDone
+    TestIntervals.bpl(11,5): anon2
+    TestIntervals.bpl(12,14): anon10_Then
+    TestIntervals.bpl(13,3): anon4
+    TestIntervals.bpl(13,14): anon11_Then
+    TestIntervals.bpl(14,3): anon6
+    TestIntervals.bpl(14,14): anon12_Then
+    TestIntervals.bpl(17,5): anon8
+    TestIntervals.bpl(21,3): Next
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/aitest9/runtest.bat b/Test/aitest9/runtest.bat
new file mode 100644
index 00000000..bafa6961
--- /dev/null
+++ b/Test/aitest9/runtest.bat
@@ -0,0 +1,11 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (VarMapFixPoint.bpl TestIntervals.bpl) do (
+  echo. 
+  echo -------------------- %%f -------------------- 
+  %BPLEXE% %* %%f /infer:i
+)