Improve default type sizes check error msg for fromIeeeBitvector() and add more info about CVC5 exception for the same method

Author: BaierD

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -15,6 +15,7 @@
 import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
+import org.sosy_lab.common.MoreStrings;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -249,8 +250,12 @@ public FloatingPointFormula fromIeeeBitvector(
     BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber);
     Preconditions.checkArgument(
         bvType.getSize() == pTargetType.getTotalSize(),
-        "The total size of the used FloatingPointType has to match the size of the bitvector"
-            + " given");
+        MoreStrings.lazyString(
+            () ->
+                String.format(
+                    "The total size of the used FloatingPointType %s has to match the size of "
+                        + "the bitvector argument %s",
+                    pTargetType.getTotalSize(), bvType.getSize())));
     return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType));
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java

@@ -417,7 +417,9 @@ protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetT
               pTargetType.getMantissaSize() + 1), // add sign bit
           pBitvector);
     } catch (CVC5ApiException cvc5ApiException) {
-      // This seems to only be thrown for wrong exponent and mantissa sizes
+      // This seems to only be thrown for wrong exponent and mantissa sizes (e.g. negative
+      // numbers, size not equal to BV size etc.). We check for this beforehand, so this should
+      // not be thrown.
       throw new RuntimeException(cvc5ApiException);
     }
   }