anchor.diff:          solve_t env ({problem with lhs=t1}) wl
   
         | Tm_match (s1, brs1), Tm_match (s2, brs2) ->
  +        let by_smt () =
  +            // using original WL
  +            let guard, wl = guard_of_prob env wl problem t1 t2 in
  +            solve env (solve_prob orig (Some guard) [] wl)
  +        in
           let rec solve_branches wl brs1 brs2 : option<(list<prob> * worklist)> =
               match brs1, brs2 with
               | br1::rs1, br2::rs2 ->
  
positive.code:                 Success (ds, imp)
              | Failed _ ->
                  UF.rollback tx;
                  by_smt wl
              end
          end
  
  
negative.code:                 let w2 = BU.map_opt w2 (SS.subst s) in
                  let e2 = SS.subst s e2 in
  
                  let scope = List.map S.mk_binder <| S.pat_bvs p1 in
  
                  (* Subproblem for then `when` clause *)
                  BU.bind_opt (
  