diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py
index 5fb24f58d..fc6605e0b 100644
--- a/claripy/backends/backend_z3.py
+++ b/claripy/backends/backend_z3.py
@@ -550,6 +550,9 @@ def _abstract_internal(self, ctx, ast, split_on=None):
             l.error(err)
             raise BackendError(err)
 
+        if ty is FP and isinstance(args[0], RM):
+            args = [*args[1:], args[0]]
+
         if op_name == "If":
             # If is polymorphic and thus must be handled specially
             ty = type(args[1])