Cubicle 1.1.2 documentation and source : Approx.remove_bad

let rec remove_bad_candidates sys faulty candidates =
  let trace = faulty.from in
  let cand = Node.origin faulty in
  let nc = 
    List.fold_left 
      (fun acc c' ->
	if node_same cand c'
	then
	  (* raise UNSAFE if we try to remove a candidate 
	     which is an unsafe property *)
	  if List.exists (node_same c') sys.t_unsafe then
	    raise (Safety.Unsafe faulty)
	  else (register_bad sys c' trace; acc)
        else 
          if Forward.spurious_due_to_cfm sys faulty then
            (* Find out if bactrack is due to crash failure model, in which
               case record literals that do not respect CMF model *)
            begin
              non_cfm_literals := SA.union (Node.litterals cand) !non_cfm_literals;
              if not quiet && verbose > 0 then 
                eprintf "Non CFM literals = %a@." SAtom.print !non_cfm_literals;
              remove_non_cfm_cand sys acc
            end
          else
            (* remove candidates that are reachable on the same trace modulo
               renaming of parameters *)
            if Forward.reachable_on_trace_from_init sys c' trace <> 
                 Forward.Unreach
	    then
              (register_bad sys c' []; acc)
	    else begin
              (* This candidate seems ok, reset its delete flag *)
              c'.deleted <- false;
              c'::acc
            end
      ) [] candidates in
  List.rev nc