diff options
| author |  Rustan Leino <leino@microsoft.com> | 2016-02-12 16:47:51 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2016-02-12 16:47:51 -0800 |
| commit | 7ce69481c0b6af79a6d6542989832cd90fc5690f (patch) | |
| tree | a91488b8ad92bc69718f2d5fda1d44082a3959de /Source/AbsInt/IntervalDomain.cs | |
| parent | abee810ceedbf551194788164fdf723edc511c0c (diff) | |
| parent | 5fb565e439255ede7dc3653708af41678b6c1062 (diff) | |
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Source/AbsInt/IntervalDomain.cs')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 8 |
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: |