1 files changed, 8 insertions, 1 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 15ff87db..c0966256 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2168,7 +2168,8 @@ namespace Microsoft.Boogie {
   public class ArithmeticCoercion : IAppliable {
     public enum CoercionType {
       ToInt,
-      ToReal
+      ToReal,
+      ToFloat
     }
 
     private IToken/*!*/ tok;
@@ -2195,6 +2196,12 @@ namespace Microsoft.Boogie {
           this.argType = Type.Int;
           this.hashCode = 2;
           break;
+        case CoercionType.ToFloat:
+          this.name = "float";
+          this.type = Type.Real;
+          this.argType = Type.Int;
+          this.hashCode = 3;
+          break;
         default:
           Contract.Assert(false);
           break;