anchor.diff:              | [], [] -> Some []
               | _ -> None
           in
  +        let by_smt () =
  +            let guard = guard_of_prob env problem t1 t2 in
  +            solve env (solve_prob orig guard [] wl)
  +        in
           begin match solve_branches brs1 brs2 with
           | None ->
  -            giveup env "Tm_match branches don't match" orig
  +            if wl.smt_ok
  +            then by_smt ()
  +            else giveup env "Tm_match branches don't match" orig
           | Some sub_probs ->
               let sub_probs = sc_prob::sub_probs in
               let formula = U.mk_conj_l (List.map (fun p -> fst (p_guard p)) sub_probs) in
  +            let tx = UF.new_transaction () in
               let wl = solve_prob orig (Some formula) [] wl in
  -            solve env (attempt sub_probs wl)
  +            begin match solve env (attempt sub_probs ({wl with smt_ok = false})) with
  +            | Success ds ->
  +                UF.commit tx;
  +                Success ds
  +            | Failed _ ->
  +                UF.rollback tx;
  +                by_smt ()
  +            end
           end
   
         | Tm_match _, _
  
positive.code:                     | _ -> false
                  in
                  if (may_relate head1 || may_relate head2) && wl.smt_ok
                  then let guard =
                          if problem.relation = EQ
                          then mk_eq2 orig t1 t2
                          else let has_type_guard t1 t2 =
                                  match problem.element with
                                      | Some t -> U.mk_has_type t1 t t2
                                      | None ->
                                      let x = S.new_bv None t1 in
                                      let u_x = env.universe_of env t1 in
                                      U.mk_forall u_x x (U.mk_has_type t1 (S.bv_to_name x) t2) in
                               if problem.relation = SUB
                               then has_type_guard t1 t2
                               else has_type_guard t2 t1 in
                      solve env (solve_prob orig (Some guard) [] wl)
                  else giveup env (BU.format2 "head mismatch (%s vs %s)" (Print.term_to_string head1) (Print.term_to_string head2)) orig
  
              | (_, Some (t1, t2)) -> //heads match after some delta steps
  
negative.code:         then let ref_prob = TProb <| mk_problem (p_scope orig @ [mk_binder x1]) orig phi1 EQ phi2 None "refinement formula" in
               begin match solve env ({wl with defer_ok=false; attempting=[ref_prob]; wl_deferred=[]}) with
                     | Failed _ -> fallback()
                     | Success _ ->
                         let guard =
                           U.mk_conj (p_guard base_prob |> fst)
                                     (p_guard ref_prob |> fst |> guard_on_element wl problem x1) in
  