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:         t, wl
        end
      | _ ->
        failwith "impossible"
  
  (* Only call if ensure_no_uvar_subst was called on t before *)
  let destruct_flex_t' t : flex_t =
  
negative.code:     | _ -> failwith "Not a flex-uvar"
  
  (* Make sure the uvar at the head of t0 is not affected by a
   * the substitution in the Tm_uvar node.
   *
   * 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 by making a new variable with
   * that is "hoisted" and which we apply to the binders of the original
   * uvar. There is an optimization in place to hoist as few binders as
   * possible.
   *
   * Example: If we have ((x:a),(y:b),(z:c) |- ?u : ty)[y <- 42], we will
   * make ?u' with x in its binders, abstracted over y and z:
   *
   * (x |- ?u') : b -> c -> ty
   *
   * (we keep x since it's unaffected by the substitution; z is not since
   * it has y in scope) and then solve
   *
   * ?u <- (?u' y z)
   *
   * Which means the original term now compresses to ?u' 42 z. The flex
   * problem we now return is
   *
   * ?u', [42 z]
   *
   * We also return early if the substitution is empty or if the uvar is
   * totally unaffected by it.
   *)
  let ensure_no_uvar_subst (t0:term) (wl:worklist)
    : term * worklist
    = (* Returns true iff the variable x is not affected by substitution s *)
      let bv_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
  