let backtrack (selection_lookahead: selection_lookahead) : unit =
  (* for each index... *)
  selection_lookahead.sl_candidates#iter
    (fun _ index ->
       (* ... find all invalid entries *)
       let remove_entries =
         index#fold
           (fun acc term raw_context_unifier ->
              if Context_unifier.is_raw_context_unifier_invalid raw_context_unifier then
                (term, raw_context_unifier) :: acc
              else
                acc
           )
           []
       in
         (* ... and remove them *)
         List.iter
           (fun (term, raw_context_unifier) ->
              if not (index#remove term (Some raw_context_unifier)) then begin
                print_endline (Term.term_to_string term);
                print_endline (Context_unifier.raw_context_unifier_to_string raw_context_unifier);
                failwith "Selection_lookahead.backtrack"
              end;
              selection_lookahead.sl_size <- selection_lookahead.sl_size - 1;
           )
           remove_entries
    )