summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/AbsInt/IntervalDomain.cs4
-rw-r--r--Test/aitest0/Intervals.bpl15
-rw-r--r--Test/aitest0/Intervals.bpl.expect2
3 files changed, 20 insertions, 1 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index ee9d632b..2fd37463 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -884,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
Lo = BigInteger.Zero;
Hi = hi1;
+ if (lo0 < lo1 && hi0 != null && hi0 < lo1) {
+ Lo = lo0;
+ Hi = hi0;
+ }
}
break;
case BinaryOperator.Opcode.RealDiv:
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