diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp
index 21fd341d538..e3018465901 100644
--- a/src/goto-programs/goto_inline.cpp
+++ b/src/goto-programs/goto_inline.cpp
@@ -122,6 +122,11 @@ void goto_inlinet::parameter_assignments(
         {
           actual.make_typecast(par_type);
         }
+        else if(f_partype.id()==ID_floatbv &&
+                f_acttype.id()==ID_floatbv)
+        {
+          actual.make_typecast(par_type);
+        }
         else
         {
           error().source_location=actual.find_source_location();