From e25dac8edab3e3f23db7c83b393ed388840d239f Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Tue, 17 Nov 2015 14:03:06 -0600
Subject: Fix issue #25.

---
 Test/aitest0/Issue25.bpl        | 14 ++++++++++++++
 Test/aitest0/Issue25.bpl.expect |  8 ++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 Test/aitest0/Issue25.bpl
 create mode 100644 Test/aitest0/Issue25.bpl.expect

(limited to 'Test')

diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl
new file mode 100644
index 00000000..6ffcd113
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+const N: int;
+axiom 0 <= N;
+
+procedure vacuous_post()
+ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25).
+{
+var x: int;
+x := -N;
+while (x != x) {
+}
+}
diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect
new file mode 100644
index 00000000..80eeb1a7
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl.expect
@@ -0,0 +1,8 @@
+Bug25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+Bug25.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    Bug25.bpl(11,3): anon0
+    Bug25.bpl(12,1): anon2_LoopHead
+    Bug25.bpl(12,1): anon2_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3