diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:22:03 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:22:03 -0600 |
commit | dd8e69b7b71a9375b7206a70633deae234175ef8 (patch) | |
tree | 3ec3a9796afb6ce8c808a407c672237ce94f4b78 /Test/aitest0/Intervals.bpl | |
parent | 1c16dc829c81426e17427c0d103ed831a48f1f81 (diff) |
Improve precision of abstract interpreter for modulo operations.
Diffstat (limited to 'Test/aitest0/Intervals.bpl')
-rw-r--r-- | Test/aitest0/Intervals.bpl | 15 |
1 files changed, 15 insertions, 0 deletions
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; +} |