diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2015-09-23 04:08:00 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2015-09-23 04:08:00 -0600 |
| commit | 80f3d4ed1bb221adbd3c7162acea10920b9fab73 (patch) | |
| tree | 218275e91b58fdb3cbce0376a4b423fa34e4e763 /Source/VCExpr | |
| parent | 28a20e6eba2919e008f70874b4c12a3ce7ad049c (diff) | |
Modified BigFloat to avoid evaluating the floating point value before sending it to z3
Diffstat (limited to 'Source/VCExpr')
| -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);
|