diff options
Diffstat (limited to 'Source/VCExpr/VCExprASTPrinter.cs')
| -rw-r--r-- | Source/VCExpr/VCExprASTPrinter.cs | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 8b79b0e5..00e6fb9c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -302,12 +302,6 @@ 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);
@@ -353,12 +347,6 @@ 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);
|