From d67336874fda05a7e7cca7ed3323b8b76d04b364 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 18 Dec 2016 23:30:25 +0000
Subject: [PATCH] Cast floatbv arguments to parameter types on inlining

---
 src/goto-programs/goto_inline.cpp | 5 +++++
 1 file changed, 5 insertions(+)

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();