let extend_context lemmas_propositional element =
  let literal =
    element.Context.el_literal
  in
  let contradictory =
    (lemmas_propositional.subsumed#find (Term.request_negated_literal literal))#find_all_instances
      ~p_preserving:true literal.Term.atom
  in
    List.iter
      (fun abstraction ->
         match abstraction.abs_status with
           | True _ ->
               print_endline (Term.literal_to_string abstraction.abs_literal ^ " : True");
               failwith "extend_context 1"

           | False _ ->
               ()

           | Undetermined ->
               abstraction.abs_status <- False element;

               begin
                 try
                   let lemmas =
                     AbstractionTable.find lemmas_propositional.abstraction_to_lemmas abstraction
                   in
                     LemmaTable.iter
                       (fun lemma _ -> compute_propagation lemmas_propositional lemma)
                       lemmas
                 with
                   | Not_found ->
                       (* not used as a watched literal *)
                       () 
               end
      )
      contradictory;

  let subsumed =
    (lemmas_propositional.subsumed#find literal)#find_all_instances
      ~p_preserving:true literal.Term.atom
  in
    List.iter
      (fun abstraction ->
         match abstraction.abs_status with
           | True _ ->
               ()

           | False _ ->
               failwith "extend_context 2"

           | Undetermined ->
               abstraction.abs_status <- True element;
      )
      subsumed;

    ()