Fixed bug in abstract interpretation over reals

2 files changed, 15 insertions, 1 deletions

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;

+  }

+}