anchor.diff:              | [], [] -> Some ([], wl)
               | _ -> None
           in
  -        let by_smt wl =
  -            let guard, wl = guard_of_prob env wl problem t1 t2 in
  -            solve env (solve_prob orig (Some guard) [] wl)
  -        in
           begin match solve_branches wl brs1 brs2 with
           | None ->
               if wl.smt_ok
  -            then by_smt wl
  +            then by_smt ()
               else giveup env "Tm_match branches don't match" orig
           | Some (sub_probs, wl) ->
               let sc_prob, wl = mk_t_problem wl [] orig s1 EQ s2 None "match scrutinee" in
  
positive.code:         solve_t env ({problem with lhs=t1}) wl
  
        | Tm_match (s1, brs1), Tm_match (s2, brs2) ->
          let rec solve_branches wl brs1 brs2 : option<(list<prob> * worklist)> =
              match brs1, brs2 with
              | br1::rs1, br2::rs2 ->
  
negative.code:                 Success (ds, imp)
              | Failed _ ->
                  UF.rollback tx;
                  by_smt ()
              end
          end
  
  