From 818c4c2849d9c9cd3fb674458249a353cf41009a Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Fri, 28 Jun 2019 18:11:05 -0600
Subject: [PATCH] Fixed BigFloat construction of the returned FP constants

---
 Source/Provers/SMTLib/ProverInterface.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d21b02e10..eea6fbe86 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -2456,7 +2456,7 @@ public override object Evaluate(VCExpr expr)
             BigInteger exp = getBvVal(expExpr);
             int expSize = getBvSize(expExpr);
             BigInteger sig = getBvVal(sigExpr);
-            int sigSize = getBvSize(sigExpr);
+            int sigSize = getBvSize(sigExpr)+1;
             return new Basetypes.BigFloat(isNeg, sig, exp, sigSize, expSize);
         }
         if (resp.Name == "_" && resp.ArgCount == 3)