Special case RM position in z3 backend

Author: twizmwazin

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])