summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/AbsInt/IntervalDomain.cs4
1 files changed, 4 insertions, 0 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: