FP: improve error message and add test for it.

Author: kfriedberger

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

@@ -266,9 +266,8 @@ public FloatingPointFormula fromIeeeBitvector(
         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())));
+                    "The total size %s of type %s has to match the size %s of type %s.",
+                    pTargetType.getTotalSize(), pTargetType, bvType.getSize(), bvType)));
     return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType));
   }
 

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -1098,6 +1098,27 @@ public void checkString2FpConversion64() throws SolverException, InterruptedExce
                 fpmgr.makeNumber(Double.toString(pDouble), doublePrecType)));
   }
 
+  @Test
+  public void checkErrorOnInvalidSize_IeeeBv2FpConversion() {
+    BitvectorFormula bv = bvmgr.makeBitvector(9, 123);
+
+    var exSingle =
+        assertThrows(
+            IllegalArgumentException.class, () -> fpmgr.fromIeeeBitvector(bv, singlePrecType));
+    assertThat(exSingle.getMessage())
+        .contains(
+            "The total size 32 of type FloatingPoint<exp=8,mant=23> "
+                + "has to match the size 9 of type Bitvector<9>.");
+
+    var exDouble =
+        assertThrows(
+            IllegalArgumentException.class, () -> fpmgr.fromIeeeBitvector(bv, doublePrecType));
+    assertThat(exDouble.getMessage())
+        .contains(
+            "The total size 64 of type FloatingPoint<exp=11,mant=52> "
+                + "has to match the size 9 of type Bitvector<9>.");
+  }
+
   @Test
   public void checkIeeeBv2FpConversion32() throws SolverException, InterruptedException {
     proveForAll(