1 files changed, 12 insertions, 0 deletions
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 00e6fb9c..8b79b0e5 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -302,6 +302,12 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return PrintNAry("/", node, wr);
     }
+    public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("/f", node, wr);
+    }
     public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
       //Contract.Requires(wr != null);
       //Contract.Requires(node != null);
@@ -347,6 +353,12 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return PrintNAry("real", node, wr);
     }
+    public bool VisitToFloatOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("float", node, wr);
+    }
     public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
       //Contract.Requires(wr != null);
       //Contract.Requires(node != null);