anchor.diff:                [] //no guard for the unit pattern; it's a singleton
   
               | Pat_constant _c, Tm_constant c ->
  -              [U.mk_eq2 U_zero (tc_constant env pat_exp.pos c) scrutinee_tm pat_exp]
  +
  +              [U.mk_eq2 U_zero (tc_constant env pat_exp.pos c) (force_scrutinee()) pat_exp]
   
               | Pat_constant (FStar.Const.Const_int(_, Some _)), _ ->
                 //machine integer pattern, cf. #1572
                 let _, t, _ = env.type_of env pat_exp in
  -              [U.mk_eq2 U_zero t scrutinee_tm pat_exp]
  +              [U.mk_eq2 U_zero t (force_scrutinee()) pat_exp]
   
               | Pat_cons (_, []), Tm_uinst _
               | Pat_cons (_, []), Tm_fvar _ ->
  
positive.code:                 let f = head_constructor pat_exp in
                  if not (Env.is_datacon env f.v)
                  then failwith "Impossible: nullary patterns must be data constructors"
                  else discriminate scrutinee_tm (head_constructor pat_exp)
  
              | Pat_cons (_, pat_args), Tm_app(head, args) ->
                  //application pattern
  
negative.code:                         List.mapi (fun i ((pi, _), (ei, _)) ->
                              let projector = Env.lookup_projector env f.v i in
                              //NS: TODO ... should this be a marked as a record projector? But it doesn't matter for extraction
                              let scrutinee_tm =
                                  match Env.try_lookup_lid env projector with
                                  | None ->
                                    None //no projector, e.g., because we are actually typechecking the projector itself
                                  | _ ->
                                    let proj = S.fvar (Ident.set_lid_range projector f.p) (Delta_equational_at_level 1) None in
                                    Some (mk_Tm_app proj [as_arg (force_scrutinee())] None f.p)
                              in
                              build_branch_guard scrutinee_tm pi ei) |>
                          List.flatten
                       in
                       discriminate (force_scrutinee()) f @ sub_term_guards
  
              | Pat_dot_term _, _ -> []
                //a non-pattern sub-term computed via unification; no guard needeed since it is from a dot pattern
  