summaryrefslogtreecommitdiff
path: root/Source/AbsInt
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2016-03-17 13:01:10 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2016-03-17 13:01:10 -0600
commit51b7e8146f413b83a412572fcc9e3a1a8b302b79 (patch)
tree9ef4e6b21037425827b72cff1095398dc299f569 /Source/AbsInt
parent6ac996211d6f42f0c7f61ea108388d6bb798ecf8 (diff)
modified floating point syntax and modified floating point constants to use bitvector values
Diffstat (limited to 'Source/AbsInt')
-rw-r--r--Source/AbsInt/IntervalDomain.cs6
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0c954f9a..d5a5efc9 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -695,10 +695,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
Lo = floor;
Hi = ceiling;
} else if (node.Val is BigFloat) {
- BigInteger floor, ceiling;
+ BigNum floor, ceiling;
((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
- Lo = floor;
- Hi = ceiling;
+ Lo = floor.ToBigInteger;
+ Hi = ceiling.ToBigInteger;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true