anchor.diff:               | x::xs -> if f x xs then x::(filter' f xs) else filter' f xs
           in
           let sub_goals = filter' (fun g goals -> not (checkone g.witness goals)) sub_goals in
  +        bind (add_goal_from_guard goal.context guard goal.opts) (fun _ ->
  +        bind (add_goal_from_guard goal.context g   goal.opts) (fun _ ->
           bind (add_irrelevant_goal goal.context pre goal.opts) (fun _ ->
           // Try to discharge the precondition, which is often trivial
           bind (trytac trivial) (fun _ ->
  -        add_goals sub_goals)))))
  +        add_goals sub_goals))))))))
   
   let destruct_eq' (typ : typ) : option<(term * term)> =
       match U.destruct_typ_as_formula typ with
  
positive.code:     | [] -> fail "No more goals (1)"
      | hd::tl -> ret hd)
  
  let add_irrelevant_goal (env:env) (phi:typ) opts : tac<unit> =
      let typ = U.mk_squash phi in
      bind (new_uvar env typ) (fun u ->
      let goal = { context = env; witness = u; goal_ty = typ; opts = opts } in
      add_goals [goal])
  
  let smt : tac<unit> =
      bind cur_goal (fun g ->
  
negative.code: module Print = FStar.Syntax.Print
  module TcUtil = FStar.TypeChecker.Util
  module TcTerm = FStar.TypeChecker.TcTerm
  module TcComm = FStar.TypeChecker.Common
  module N = FStar.TypeChecker.Normalize
  module RD = FStar.Reflection.Data
  module UF = FStar.Syntax.Unionfind
  