summaryrefslogtreecommitdiff
path: root/Source/AbsInt
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AbsInt')
-rw-r--r--Source/AbsInt/IntervalDomain.cs8
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0d2676f2..2fd37463 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -698,9 +698,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
lo = Lo; hi = Hi;
if (hi != null) {
Lo = node.Type.IsReal ? -hi : 1 - hi;
+ } else {
+ Lo = null;
}
if (lo != null) {
Hi = node.Type.IsReal ? -lo : 1 - lo;
+ } else {
+ Hi = null;
}
}
else if (op.Op == UnaryOperator.Opcode.Not) {
@@ -880,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: