1 files changed, 1 insertions, 4 deletions
diff --git a/backend/LTL.v b/backend/LTL.v
index 48c5c850..bb596fa2 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -111,10 +111,7 @@ Definition call_regs (caller: locset) : locset :=
 Definition return_regs (caller callee: locset) : locset :=
   fun (l: loc) =>
     match l with
-    | R r =>
-        if In_dec mreg_eq r destroyed_at_call
-        then callee (R r)
-        else caller (R r)
+    | R r => if is_callee_save r then caller (R r) else callee (R r)
     | S sl ofs ty => caller (S sl ofs ty)
     end.