let build_periodicity_cstrs prec_cstrs choice =
  let iof_vars = vars_of_linear_constraints prec_cstrs in
  let periodicity_cstrs =
    Integer_var_set.fold
      (fun var per_cstrs ->
        match var with
        | Iof (c_n, iof_p_n_j) ->
            let nbones_c_n_u, nbones_c_n_v =
              Word_var_map.find c_n choice.nbones_env
            in
            if iof_p_n_j > nbones_c_n_u + nbones_c_n_v then
              build_periodicity_cstr var (nbones_c_n_u, nbones_c_n_v) ::
              per_cstrs
            else
              per_cstrs
        | _ -> assert false)
      iof_vars []
  in
  List.rev periodicity_cstrs