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.

---
 Source/AbsInt/IntervalDomain.cs |  4 ++++
 Test/aitest0/Issue25.bpl        | 14 ++++++++++++++
 Test/aitest0/Issue25.bpl.expect |  8 ++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 Test/aitest0/Issue25.bpl
 create mode 100644 Test/aitest0/Issue25.bpl.expect

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0d2676f2..ee9d632b 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -698,9 +698,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
             lo = Lo; hi = Hi;
             if (hi != null) {
               Lo = node.Type.IsReal ? -hi : 1 - hi;
+            } else {
+              Lo = null;
             }
             if (lo != null) {
               Hi = node.Type.IsReal ? -lo : 1 - lo;
+            } else {
+              Hi = null;
             }
           }
           else if (op.Op == UnaryOperator.Opcode.Not) {
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