From 2dae113e5996e050ca6595542de5030747245929 Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 27 Apr 2015 05:37:19 -0600
Subject: Began adding the float type to VC expression

---
 Source/VCExpr/Boogie2VCExpr.cs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'Source/VCExpr/Boogie2VCExpr.cs')

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 8674f8c0..aa246c37 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST {
         return Gen.Integer(node.asBigNum);
       } else if (node.Val is BigDec) {
         return Gen.Real(node.asBigDec);
-      } else if (node.Val is BvConst) {
+      } else if (node.Val is BigFloat) {
+        return Gen.Float(node.asBigFloat);
+      }
+      else if (node.Val is BvConst) {
         return Gen.Bitvector((BvConst)node.Val);
       } else {
         System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
@@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST {
         if (cce.NonNull(e.Type).IsInt) {
           return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
         }
-        else {
+        else if (cce.NonNull(e.Type).IsReal) {
           return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
         }
+        else  {//is float
+          return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO), e);
+        } 
       }
       else {
         return Gen.Not(this.args);
-- 
cgit v1.2.3