From dd8e69b7b71a9375b7206a70633deae234175ef8 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Mon, 28 Dec 2015 20:22:03 -0600
Subject: Improve precision of abstract interpreter for modulo operations.

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

(limited to 'Test')

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index fddce05a..8d40b81d 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -332,3 +332,18 @@ procedure W0(N: real)
     assert N - i <= bf0 - 1.0;
   }
 }
+
+// mod
+
+procedure Mod0(n: int)
+  requires 10 < n;
+{
+    var i: int;
+
+    i := 0;
+    while (i < 10)
+    {
+        i := (i mod n) + 1;
+    }
+    assert i == 10;
+}
diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect
index a0769ec5..980593a9 100644
--- a/Test/aitest0/Intervals.bpl.expect
+++ b/Test/aitest0/Intervals.bpl.expect
@@ -54,4 +54,4 @@ Execution trace:
     Intervals.bpl(303,3): anon3_LoopHead
     Intervals.bpl(303,3): anon3_LoopDone
 
-Boogie program verifier finished with 16 verified, 11 errors
+Boogie program verifier finished with 17 verified, 11 errors
-- 
cgit v1.2.3