Merge pull request boogie-org#135 from shaobo-he/fix-fp-const-str

Fixed BigFloat construction of the returned FP constants
alexanderjsummers · Jul 1, 2019 · 5c829b6 · 5c829b6
2 parents 6c6cfb9 + 818c4c2
commit 5c829b6
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)