anchor.diff:        then Errors.diag (Env.get_range env)
                          (BU.format1 "Before normalization VC=\n%s\n" (Print.term_to_string vc));
         let vc = N.normalize [N.Eager_unfolding; N.Simplify; N.Primops] env vc in
  +      if Env.debug env <| Options.Other "Norm"
  +      || Env.debug env <| Options.Other "SMTQuery"
  +      then Errors.diag (Env.get_range env)
  +                       (BU.format1 "After normalization VC=\n%s\n" (Print.term_to_string vc));
         match check_trivial vc with
         | Trivial -> Some ret_g
         | NonTrivial vc ->
  
positive.code:                                          (BU.format2 "Trying to solve:\n> %s\nWith proof_ns:\n %s\n"
                                                   (Print.term_to_string goal)
                                                   (Env.string_of_proof_ns env));
                          let res = env.solver.solve use_env_range_msg env goal in
                          FStar.Options.pop ();
                          res
  
negative.code:                         env.solver.preprocess env vc
                      )
                  end
                  else [env,vc,FStar.Options.peek ()]
              in
              vcs |> List.iter (fun (env, goal, opts) ->
                      let goal = N.normalize [N.Simplify; N.Primops] env goal in
                      match check_trivial goal with
  