anchor.diff:          U.close_forall_no_univs (List.rev closing) q, bindings
       in
       let env_decls, env = encode_env_bindings env bindings in
  -    if debug tcenv Options.Low
  +    if debug tcenv Options.Medium
       || debug tcenv <| Options.Other "SMTEncoding"
       || debug tcenv <| Options.Other "SMTQuery"
       then BU.print1 "Encoding query formula: %s\n" (Print.term_to_string q);
  
positive.code: let encode_modul tcenv modul =
      if Options.lax() && Options.ml_ish() then () else
      let name = BU.format2 "%s %s" (if modul.is_interface then "interface" else "module")  modul.name.str in
      if Env.debug tcenv Options.Low
      then BU.print2 "+++++++++++Encoding externals for %s ... %s exports\n" name (List.length modul.exports |> string_of_int);
      let env = get_env modul.name tcenv in
      let encode_signature (env:env_t) (ses:sigelts) =
  
negative.code:          [Module(name, Caption msg::decls@[Caption ("End " ^ msg)])]
      else decls in
      set_env ({env with warn=true});
      if Env.debug tcenv Options.Medium then BU.print1 "Done encoding externals for %s\n" name;
      let decls = caption decls in
      Z3.giveZ3 decls
  
  