From 25fca02e1deb9e60e6e330803731c9b4fcd45d34 Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 18 May 2015 22:08:43 -0600
Subject: added interpretation of floating point constants to the parser

---
 Source/VCExpr/Boogie2VCExpr.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index aa246c37..942116eb 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -1009,7 +1009,7 @@ namespace Microsoft.Boogie.VCExprAST {
           return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
         }
         else  {//is float
-          return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO), e);
+          return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e);
         } 
       }
       else {
-- 
cgit v1.2.3