src/HOL/Tools/Nitpick/nitpick.ML

      destroy_constrs: bool,
      specialize: bool,
      star_linear_preds: bool,
      fast_descrs: bool,
      peephole_optim: bool,
+     datatype_sym_break: int,
+     kodkod_sym_break: int,
      timeout: Time.time option,
      tac_timeout: Time.time option,
      max_threads: int,
      show_datatypes: bool,
      show_consts: bool,

    destroy_constrs: bool,
    specialize: bool,
    star_linear_preds: bool,
    fast_descrs: bool,
    peephole_optim: bool,
+   datatype_sym_break: int,
+   kodkod_sym_break: int,
    timeout: Time.time option,
    tac_timeout: Time.time option,
    max_threads: int,
    show_datatypes: bool,
    show_consts: bool,

 *)
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
          verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
          destroy_constrs, specialize, star_linear_preds, fast_descrs,
-         peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
-         evals, formats, atomss, max_potential, max_genuine, check_potential,
-         check_genuine, batch_size, ...} = params
+         peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout,
+         max_threads, show_datatypes, show_consts, evals, formats, atomss,
+         max_potential, max_genuine, check_potential, check_genuine, batch_size,
+         ...} = params
     val state_ref = Unsynchronized.ref state
     val pprint =
       if auto then
         Unsynchronized.change state_ref o Proof.goal_message o K
         o Pretty.chunks o cons (Pretty.str "") o single

             |> unsound_delay_for_timeout
           else
             0
         val settings = [("solver", commas_quote kodkod_sat_solver),
                         ("bit_width", string_of_int bit_width),
-                        ("symmetry_breaking", "20"),
+                        ("symmetry_breaking", string_of_int kodkod_sym_break),
                         ("sharing", "3"),
                         ("flatten", "false"),
                         ("delay", signed_string_of_int delay)]
         val plain_rels = free_rels @ other_rels
         val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels

                                            rel_table datatypes
         val declarative_axioms = plain_axioms @ dtype_axioms
         val univ_card = Int.max (univ_card nat_card int_card main_j0
                                      (plain_bounds @ sel_bounds) formula,
                                  main_j0 |> bits > 0 ? Integer.add (bits + 1))
-        val built_in_bounds = bounds_for_built_in_rels_in_formula debug
+        val built_in_bounds = bounds_for_built_in_rels_in_formula debug ofs
                                   univ_card nat_card int_card main_j0 formula
         val bounds = built_in_bounds @ plain_bounds @ sel_bounds
                      |> not debug ? merge_bounds
         val highest_arity =
           fold Integer.max (map (fst o fst) (maps fst bounds)) 0