Special case RM position in z3 backend

angr · Sep 21, 2024 · f21b9df · f21b9df
1 parent 29e5800
commit f21b9df
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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])