Changed the prover interface to report traces for time outs and out of memory.

1 files changed, 25 insertions, 0 deletions

diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl
new file mode 100644
index 00000000..c74e9320
--- /dev/null
+++ b/Test/test2/Timeouts0.bpl
@@ -0,0 +1,25 @@
+procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)

+  requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);

+  requires 0 < len;

+  ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);

+{

+    var i : int;

+

+    i := 0;

+    out[i] := 0;

+    while (i < len)

+      invariant 0 <= i && i <= len;

+      invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);

+    {

+        out[i + 1] := out[i] + 1;

+        i := i + 1;

+    }

+

+    i := 0;

+    while (i < len)

+      invariant 0 <= i && i <= len;

+      invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);

+    {

+        i := i + 1;

+    }

+}