Fixed BigFloat construction of the returned FP constants

alexanderjsummers · Jun 29, 2019 · 818c4c2 · 818c4c2
1 parent 6c6cfb9
commit 818c4c2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)