summaryrefslogtreecommitdiff
path: root/Source/VCExpr/VCExprASTVisitors.cs
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2015-09-17 03:14:27 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2015-09-17 03:14:27 -0600
commit28a20e6eba2919e008f70874b4c12a3ce7ad049c (patch)
tree58050f22ea944eb07620195303d757424f50b2a9 /Source/VCExpr/VCExprASTVisitors.cs
parentbb5395b35dcea5078c9b38a2f091f26256faac34 (diff)
Added initial support for float addition
Diffstat (limited to 'Source/VCExpr/VCExprASTVisitors.cs')
-rw-r--r--Source/VCExpr/VCExprASTVisitors.cs1
1 files changed, 0 insertions, 1 deletions
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 1bcce113..a1fb2ff4 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -77,7 +77,6 @@ namespace Microsoft.Boogie.VCExprAST {
Result VisitDivOp(VCExprNAry node, Arg arg);
Result VisitModOp(VCExprNAry node, Arg arg);
Result VisitRealDivOp(VCExprNAry node, Arg arg);
- Result VisitFloatDivOp(VCExprNAry node, Arg arg); //TODO: Add this to references from above and below
Result VisitPowOp(VCExprNAry node, Arg arg);
Result VisitLtOp(VCExprNAry node, Arg arg);
Result VisitLeOp(VCExprNAry node, Arg arg);