let backtrack lemmas_propositional =
  LiteralTable.iter
    (fun _ abstraction ->
       match abstraction.abs_status with
         | True element
         | False element when
             State.is_choice_point_invalid element.Context.el_choice_point ->
             abstraction.abs_status <- Undetermined

         | _ ->
             ()
    )
    lemmas_propositional.literal_to_abstraction;


  (* remove retracted propagations and see if they are still valid. *)
  let keep, remove =
    List.partition
      (fun (cp, _) ->
         if State.is_choice_point_valid cp then
           true

         else
           false
      )
      lemmas_propositional.propagations
  in
    lemmas_propositional.propagations <- keep;
    List.iter
      (fun (_, lemma) ->
         compute_propagation lemmas_propositional lemma
      )
      remove