anchor.diff:        | _, Tm_app _ ->
            let head1 = U.head_and_args t1 |> fst in
            let head2 = U.head_and_args t2 |> fst in
  +         let _ =
  +             if debug env (Options.Other "RelCheck")
  +             then BU.print3 ">> (%s)\n>>> head1 = %s\n>>> head2 = %s\n" (string_of_int problem.pid)
  +                                 (Print.term_to_string head1)
  +                                 (Print.term_to_string head2)
  +         in
            if (Env.is_interpreted env head1
                || Env.is_interpreted env head2)   //we have something like (+ x1 x2) =?= (- y1 y2)
            && wl.smt_ok
  
positive.code:             | MisMatch _ -> fail r
  
              | _ -> success n_delta r t1 t2 in
      aux true 0 t1 t2
  
  type tc =
   | T of term * (binders -> Range.range -> term)
  
negative.code:   | HeadMatch
    | FullMatch
  
  let string_of_option f = function
    | None -> "None"
    | Some x -> "Some " ^ f x
  
  let string_of_match_result = function
      | MisMatch (d1, d2) ->
          "MisMatch "
          ^ string_of_option Print.delta_depth_to_string d1
          ^ string_of_option Print.delta_depth_to_string d2
      | HeadMatch -> "HeadMatch"
      | FullMatch -> "FullMatch"
  
  let head_match = function
      | MisMatch(i, j) -> MisMatch(i, j)
      | _ -> HeadMatch
  