1 files changed, 32 insertions, 2 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 2fd37463..1d35b735 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
             }
           }
           return e;
-        } else {
-          Contract.Assert(V.TypedIdent.Type.IsReal);
+        } else if (V.TypedIdent.Type.IsReal){
           Expr e = Expr.True;
           if (Lo != null && Hi != null && Lo == Hi) {
             // produce an equality
@@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation
             }
           }
           return e;
+        } else {
+          Contract.Assert(V.TypedIdent.Type.IsFloat);
+          Expr e = Expr.True;
+          if (Lo != null && Hi != null && Lo == Hi)
+          {
+            // produce an equality
+            var ide = new IdentifierExpr(Token.NoToken, V);
+            e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));
+          }
+          else
+          {
+            // produce a (possibly empty) conjunction of inequalities
+            if (Lo != null)
+            {
+              var ide = new IdentifierExpr(Token.NoToken, V);
+              e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));
+            }
+            if (Hi != null)
+            {
+              var ide = new IdentifierExpr(Token.NoToken, V);
+              e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
+            }
+          }
+          return e;
         }
       }
     }
@@ -208,6 +231,8 @@ namespace Microsoft.Boogie.AbstractInterpretation
         return null;
       } else if (ty.IsReal) {
         return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
+      } else if (ty.IsFloat) {
+        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand));
       } else {
         Contract.Assume(ty.IsInt);
         return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
@@ -669,6 +694,11 @@ namespace Microsoft.Boogie.AbstractInterpretation
           ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
           Lo = floor;
           Hi = ceiling;
+        } else if (node.Val is BigFloat) {
+          BigInteger floor, ceiling;
+          ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
+          Lo = floor;
+          Hi = ceiling;
         } else if (node.Val is bool) {
           if ((bool)node.Val) {
             // true