diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-07 00:22:30 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-07 00:22:30 -0800 |
| commit | 75c6e95ecd3bea7c5e8d993bc28616c83f8a032b (patch) | |
| tree | dfd8ddeffa1a385680b73c0e5a69f034a610bd04 /Source/AbsInt | |
| parent | 4d582e4f413ce25ff1ec9c482b2e1750cee03727 (diff) | |
Dafny: fixed division in new interval domain
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index cf84e4bd..1a2904a4 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -699,14 +699,14 @@ namespace Microsoft.Boogie.AbstractInterpretation // this uses an incomplete approximation that could be tightened up
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
Lo = new BigInteger(0);
- Hi = lo0 - 1;
+ Hi = hi0;
}
break;
case BinaryOperator.Opcode.Mod:
// this uses an incomplete approximation that could be tightened up
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
Lo = new BigInteger(0);
- Hi = lo1;
+ Hi = hi1;
}
break;
default:
|