anchor.diff:  let find_localized_errors errs =
       errs |> List.tryFind (fun err -> match err.error_messages with [] -> false | _ -> true)
   
  -let has_localized_errors errs = Option.isSome (find_localized_errors errs)
  -
  -let report_errors settings : unit =
  +let report_errors (settings : query_settings) : unit =
       let format_smt_error msg =
         BU.format1 "SMT solver says:\n\t%s;\n\t\
                     Note: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t\
  
positive.code:              | 0, _, 0 when canceled_count > 0   -> "The SMT query timed out, you might want to increase the rlimit"
               | _, _, _                           -> "Try with --query_stats to get more details") |> Inl
          in
              
          match find_localized_errors settings.query_errors with
          | Some err ->
            // FStar.Errors.log_issue settings.query_range (FStar.Errors.Warning_SMTErrorReason, smt_error);
  
negative.code: let full_query_id settings =
      "(" ^ settings.query_name ^ ", " ^ (BU.string_of_int settings.query_index) ^ ")"
  
  let rec collect (l : list<'a>) : list<('a * int)> =
      let acc : list<('a * int)> = [] in
      let rec add_one acc x =
          match acc with
          | [] -> [(x, 1)]
          | (h, n)::t ->
              if h = x
              then (h, n+1)::t
              else (h, n) :: add_one t x
      in
      List.fold_left add_one acc l
  
  let ask_and_report_errors env all_labels prefix query suffix : unit =
      Z3.giveZ3 prefix; //feed the context of the query to the solver
  
  