diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-03-17 13:01:10 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-03-17 13:01:10 -0600 |
| commit | 51b7e8146f413b83a412572fcc9e3a1a8b302b79 (patch) | |
| tree | 9ef4e6b21037425827b72cff1095398dc299f569 /Source/Core/AbsyExpr.cs | |
| parent | 6ac996211d6f42f0c7f61ea108388d6bb798ecf8 (diff) | |
modified floating point syntax and modified floating point constants to use bitvector values
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index ad537288..6b2e1201 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -561,7 +561,7 @@ namespace Microsoft.Boogie { {
Contract.Requires(tok != null);
Val = v;
- Type = Type.GetFloatType(v.ExponentSize, v.MantissaSize);
+ Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);
if (immutable)
CachedHashCode = ComputeHashCode();
}
@@ -639,7 +639,7 @@ namespace Microsoft.Boogie { return Type.Real;
} else if (Val is BigFloat) {
BigFloat temp = (BigFloat)Val;
- return Type.GetFloatType(temp.ExponentSize, temp.MantissaSize);
+ return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);
} else if (Val is BvConst) {
return Type.GetBvType(((BvConst)Val).Bits);
} else {
|