From 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 8 Apr 2014 08:31:05 -0700
Subject: Fixed bug in abstract interpretation over reals

---
 Test/aitest0/Answer        |  2 +-
 Test/aitest0/Intervals.bpl | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

(limited to 'Test/aitest0')

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 961b3c33..cc518d1b 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -165,4 +165,4 @@ Execution trace:
     Intervals.bpl(301,3): anon3_LoopHead
     Intervals.bpl(301,3): anon3_LoopDone
 
-Boogie program verifier finished with 15 verified, 11 errors
+Boogie program verifier finished with 16 verified, 11 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 6a588bbe..c769645f 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -316,3 +316,17 @@ procedure Id17(n: int)
   assert 0 <= i;  // fine: SometimesId2 claims to be an identity and the use of it is int->int
 }
 
+// real numbers
+
+procedure W0(N: real)
+{
+  var i, bf0: real;
+  i := 0.0;
+  while (i < N) {
+    bf0 := N - i;
+    i := i + 1.0;
+    // check termination:
+    assert 0.0 <= bf0;
+    assert N - i <= bf0 - 1.0;
+  }
+}
-- 
cgit v1.2.3