implement cast bv -> floatbv

This case was missing but is used in our lowering of floating-point
operations.

Author: Daniel Kroening

regression/cbmc/Float-div3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float-equality1/test_no_equality.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Float-smt2-1/test.desc

@@ -1,4 +1,4 @@
-CORE smt-backend broken-smt-backend
+CORE smt-backend
 main.c
 --smt2
 ^EXIT=10$

regression/cbmc/Float-to-double2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

src/solvers/smt2/smt2_conv.cpp

@@ -2316,6 +2316,20 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       const typecast_exprt tmp(src, bool_typet());
       convert_typecast(typecast_exprt(tmp, dest_type));
     }
+    else if(src_type.id() == ID_bv)
+    {
+      if(
+        to_bv_type(src_type).get_width() !=
+        to_floatbv_type(dest_type).get_width())
+      {
+        UNEXPECTEDCASE("Typecast bv -> float with wrong width");
+      }
+
+      if(use_FPA_theory)
+        SMT2_TODO("FPA cast bv -> float");
+      else
+        convert_expr(src);
+    }
     else
       UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
   }