anchor.diff:                      | _ -> false
                   in
                   if (may_relate head1 || may_relate head2) && wl.smt_ok
  -                then let guard =
  -                        if problem.relation = EQ
  -                        then mk_eq2 orig t1 t2
  -                        else let has_type_guard t1 t2 =
  -                                match problem.element with
  -                                    | Some t -> U.mk_has_type t1 t t2
  -                                    | None ->
  -                                    let x = S.new_bv None t1 in
  -                                    let u_x = env.universe_of env t1 in
  -                                    U.mk_forall u_x x (U.mk_has_type t1 (S.bv_to_name x) t2) in
  -                             if problem.relation = SUB
  -                             then has_type_guard t1 t2
  -                             else has_type_guard t2 t1 in
  -                    solve env (solve_prob orig (Some guard) [] wl)
  +                then let guard = guard_of_prob env problem t1 t2 in
  +                     solve env (solve_prob orig guard [] wl)
                   else giveup env (BU.format2 "head mismatch (%s vs %s)" (Print.term_to_string head1) (Print.term_to_string head2)) orig
   
               | (_, Some (t1, t2)) -> //heads match after some delta steps
  
positive.code:         then let ref_prob = TProb <| mk_problem (p_scope orig @ [mk_binder x1]) orig phi1 EQ phi2 None "refinement formula" in
               begin match solve env ({wl with defer_ok=false; attempting=[ref_prob]; wl_deferred=[]}) with
                     | Failed _ -> fallback()
                       | Success _ ->
                         let guard =
                           U.mk_conj (p_guard base_prob |> fst)
                                     (p_guard ref_prob |> fst |> guard_on_element wl problem x1) in
  
negative.code:                 (fun wprobs ->
  
                  (* Branch body *)
                  // GM: Could use problem.relation here instead of EQ?
                  let prob = TProb <| mk_problem scope orig e1 EQ e2 None "branch body" in
                  BU.bind_opt (solve_branches rs1 rs2) (fun r ->
                  Some (prob::(wprobs @ r))))
  