let iof_and_size_cstrs_solving ?(verbose = false) cstrs =
  let add_binding x x' vars =
    if Integer_var_map.mem x vars then vars
    else Integer_var_map.add x x' vars
  in
  let cplex_var_of_integer_var x =
    match x with
    | Size (C n) -> Format.sprintf "size_c%d" n
    | Iof (C n, j) -> Format.sprintf "I_c%d_%d" n j
  in
  let sign_of_int n = if n < 0 then Cplex.Minus else Cplex.Plus in
  let cplex_term_of_linear_term (k, x) =
    let x' = cplex_var_of_integer_var x in
    (x, x'), (sign_of_int k, abs k, x')
  in
  let cplex_cmp_of_linear_cstr cstr =
    match cstr with
    | Eq _ -> Cplex.Eq
    | Le _ -> Cplex.Leq
    | Ge _ -> Cplex.Geq
  in
  let cplex_cstr_of_linear_cstr vars cstr =
    match cstr with
    | Eq (terms, c)
    | Le (terms, c)
    | Ge (terms, c) ->
        let vars, terms' =
          List.fold_left
            (fun (vars, terms') term ->
              let (x, x'), term' = cplex_term_of_linear_term term in
              add_binding x x' vars, term' :: terms')
            (vars, [])
            terms
        in
        vars, (List.rev terms', cplex_cmp_of_linear_cstr cstr, c)
  in
  let cplex_cstr_of_linear_cstrs vars cstrs =
    let vars, cplex_cstrs =
      List.fold_left
        (fun (vars, cplex_cstrs) cstr ->
          let vars, cplex_cstr = cplex_cstr_of_linear_cstr vars cstr in
          vars, cplex_cstr :: cplex_cstrs)
        (vars, []) cstrs
    in
    vars, List.rev cplex_cstrs
  in
  let vars = Integer_var_map.empty in
  let vars, synchronizability =
    cplex_cstr_of_linear_cstrs vars cstrs.synchronizability
  in
  let vars, precedence =
    cplex_cstr_of_linear_cstrs vars cstrs.precedence
  in
  let vars, periodicity =
    cplex_cstr_of_linear_cstrs vars cstrs.periodicity
  in
  let vars, sufficient_size =
    cplex_cstr_of_linear_cstrs vars cstrs.sufficient_size
  in
  let vars, sufficient_indexes =
    cplex_cstr_of_linear_cstrs vars cstrs.sufficient_indexes
  in
  let vars, increase_indexes =
    cplex_cstr_of_linear_cstrs vars cstrs.increase_indexes
  in
  let integer =
    Integer_var_map.fold (fun _ x acc -> x :: acc) vars []
  in
  let bounds =
    Integer_var_map.fold (fun _ x acc -> (Some 0, x, None) :: acc) vars []
  in
  let objective =
    let l =
      Integer_var_map.fold
        (fun x x' acc ->
          match x with
          | Iof _ -> (Cplex.Plus, 1, x') :: acc
          | Size _ -> acc) vars []
    in
    Cplex.Minimize l
  in
  let subject_to =
    synchronizability @
    precedence @
    periodicity @
    sufficient_size @
    sufficient_indexes @
    increase_indexes
  in
  let cplex_system =
    { Cplex.env = vars;
      integer = integer;
      bounds = bounds;
      objective = objective;
      subject_to = subject_to;
    }
  in
  let cplex_verbose = !Cplex.verbose in
  Cplex.verbose := verbose;
  if verbose then begin
    Format.printf "Indexes of 1s and size constraints solving:@\n  @[";
  end;
  match Cplex.solve cplex_system with
  | Cplex.GLP_OPT, cplex_sol ->
      Cplex.verbose := cplex_verbose;
      let sol =
        Integer_var_map.map
          (fun x' -> List.assoc x' cplex_sol)
          vars
      in
      if verbose then begin
        Format.printf "%a"
          fprint_linear_cstrs_sol sol;
        Format.printf "@]@\n"
      end;
      sol
  | Cplex.GLP_NOFEAS, _ -> raise Solve
  | Cplex.Empty_constraints, _ -> Integer_var_map.empty
  | _ -> assert false