let backtrack (context: context) : unit =
  (* first remove all invalid literals *)
  backtrack_elements context;
  (* now undoe the compacting of now removed literals *)
  backtrack_compact context;

  match context.universal with
    | Some cp when State.is_choice_point_invalid cp ->
        context.universal <- None
    | _ -> ()