From 80f3d4ed1bb221adbd3c7162acea10920b9fab73 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Wed, 23 Sep 2015 04:08:00 -0600 Subject: Modified BigFloat to avoid evaluating the floating point value before sending it to z3 --- Source/VCExpr/VCExprASTPrinter.cs | 12 ------------ 1 file changed, 12 deletions(-) (limited to 'Source/VCExpr') 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); -- cgit v1.2.3