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:     in
      aux bs1 bs2
  
  
  (******************************************************************************************************)
  (* Main solving algorithm begins here *)
  
negative.code:                     | _ -> false
                  in
                  if (may_relate head1 || may_relate head2) && wl.smt_ok
                  then let guard = guard_of_prob env problem t1 t2 in
                       solve env (solve_prob orig 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
  