integrated the named float type to act as a real in boogie

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 2326ba7a..4632b1e4 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1424,6 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return CastArguments(node, Type.Real, bindings, 0);

     }

+    public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)

+    {

+      Contract.Requires((bindings != null));

+      Contract.Requires((node != null));

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      return CastArguments(node, Type.Float, bindings, 0);

+    }

     public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));