let check_productive (context: context) (producer: literal) (produced: literal) : element option =

  if not (Config.productivity context.config) then begin
    None
  end

  (* must be productive if the context is not contradictory. *)
  else if Term.are_terms_variants producer.Term.atom produced.Term.atom then begin
    None
  end

  (* if the producer is universal (and not compacted) it must produce the instance
     if the context is not contradictory. *)
  else if not (Term_attributes.is_term_parametric producer.Term.atom) then begin
    None
  end

  (* do the check *)
  else begin
    let check =
      check_productive context producer produced
    in
      begin
        match check with
          | None ->
              ()
                
          | Some _ ->
              Statistic.inc_filtered_by_productivity context.statistic;
      end;
      check
  end