diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 980a927a495be4d61de6839af18a89cdb9da59f3..7f7b48a6ff9af72082e620c8c316997967322dbd 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -559,7 +559,12 @@ let mkRule_DefaultImplication sort bs defer sl : stateExpander =
 
 let mkRule_Choice sort bs defer sl : stateExpander =
   assert (List.length sl = 2);
-  let defer1 = bsetMake () in (* TODO: track deferrals *)
+  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+  let deferral_tracking defer f nextf =
+    if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+         ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+    then bsetAdd defer nextf
+  in
   let dep bsl =
     assert (List.length bsl = 2);
     let bs1 = List.nth bsl 0 in
@@ -575,17 +580,22 @@ let mkRule_Choice sort bs defer sl : stateExpander =
     res
   in
   let bs1 = bsetMake () in
+  let defer1 = bsetMakeRealEmpty () in
   let bs2 = bsetMake () in
+  let defer2 = bsetMakeRealEmpty () in
   let getRule f =
-    if lfGetType sort f = ChcF then begin
-      bsetAdd bs1 (lfGetDest1 sort f);
-      bsetAdd bs2 (lfGetDest2 sort f)
-    end else ()
+    if lfGetType sort f = ChcF then
+      begin
+        bsetAdd bs1 (lfGetDest1 sort f);
+        deferral_tracking defer1 f (lfGetDest1 sort f);
+        bsetAdd bs2 (lfGetDest2 sort f);
+        deferral_tracking defer2 f (lfGetDest2 sort f)
+      end else ()
   in
   bsetIter getRule bs;
   let s1 = List.nth sl 0 in
   let s2 = List.nth sl 1 in
-  lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1); (s2, bs2, defer1)])]
+  lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1); (s2, bs2, defer2)])]
 
 
 let mkRule_Fusion sort bs defer sl : stateExpander =