anchor.diff:        | Tm_app({n=Tm_uvar _}, _), Tm_uvar _
         | Tm_uvar _,                Tm_app({n=Tm_uvar _}, _)
         | Tm_app({n=Tm_uvar _}, _), Tm_app({n=Tm_uvar _}, _) ->
  -        (* We need to do both ensure_no_uvar_subst calls before
  -         * destructing since we might have the same uvar on
  -         * both sides. See #1616. *)
  +      (* In the case that we have the same uvar on both sides, we cannot
  +       * simply call destruct_flex_t on them, and instead we need to do
  +       * both ensure_no_uvar_subst calls before destructing.
  +       *
  +       * Calling destruct_flex_t would (potentially) first solve the
  +       * head uvar to a fresh one and then return the new one. So, if we
  +       * we were calling destruct_flex_t directly, the second call will
  +       * solve the uvar returned by the first call. We would then pass
  +       * it to to solve_t_flex_flex, causing a crash.
  +       *
  +       * See issue #1616. *)
           let t1, wl = ensure_no_uvar_subst t1 wl in
           let t2, wl = ensure_no_uvar_subst t2 wl in
           let f1 = destruct_flex_t' t1 in
  
positive.code:     | _ -> failwith "Not a flex-uvar"
  
  (* Make sure the uvar at the head of t0 is not affected by a
   * substitution.
   *
   * In the case that it is, first solve it to a new appropriate uvar
   * without a substitution. This function returns t again, though
   * it is unchanged (the changes only happen in the UF graph).
   *
   * The way we generate the new uvar is find the x's in the domain of ?u
   * that are not affected by the substitution and make a new variable with
   * only those binders in the domain. The ones that are affected we will
   * "hoist" by making the type of ?u' an arrow.
   *
   * Example:
   * If we have (x,y |- ?u : ty)[(x:a) <- x, (y:int) <- 42], we will make
   * ?u' with x in its binders, abstracted over y:
   *
   * (x |- ?u') : int -> ty
   *
   * and then solve
   *
   * ?u <- (?u' y)
   *
   * Which means the original term now compresses to ?u' 42. The flex
   * problem we now return is
   *
   * ?u', [42]
   *
   * We return early if the substitution is empty or if the uvar is
   * totally unaffected by it.
   *
   * (It's not strictly needed for this function to return t, compressing
   *  t0 will give you the same term.)
   *)
  let ensure_no_uvar_subst (t0:term) (wl:worklist)
    : term * worklist
    = (* Returns true iff the variable x is not affected by substitution s *)
      let not_affected_by (s:subst_ts) (x:bv) : bool =
        let t_x = S.bv_to_name x in
        let t_x' = SS.subst' s t_x in
        match (SS.compress t_x').n with
  
negative.code:          S.bv_eq x y // Check if substituting returned the same variable
        | _ -> false
      in
      let binding_not_affected_by (s:subst_ts) (b:binding) : bool =
        match b with
        | Binding_var x -> bv_not_affected_by s x
        | _ -> true
      in
      let head, args = U.head_and_args t0 in
      match (SS.compress head).n with
      | Tm_uvar (uv, ([], _)) ->
        (* No subst, nothing to do *)
        t0, wl
  
      | Tm_uvar (uv, _) when List.isEmpty uv.ctx_uvar_binders ->
        (* No binders in scope, also good *)
        t0, wl
  
      | Tm_uvar (uv, s) ->
        (* Obtain the maximum prefix of the binders that can remain as-is
         * (gamma is a snoc list, so we want a suffix of it. *)
        let gamma_aff, new_gamma = FStar.Common.max_suffix (binding_not_affected_by s)
                                                           uv.ctx_uvar_gamma
        in
        begin match gamma_aff with
        | [] ->
          (* Not affected by the substitution at all, do nothing *)
  