let check_iof_and_size_sol iof_and_size_cstrs iof_and_size_sol =
  let check_linear_cstr cstr sol =
    let eval terms =
      List.fold_left
        (fun acc (k, x) ->
          let v =
            try Integer_var_map.find x sol
            with Not_found -> assert false
          in
          acc + k * v)
        0
        terms
    in
    match cstr with
    | Eq (terms, n) -> eval terms = n
    | Le (terms, n) -> eval terms <= n
    | Ge (terms, n) -> eval terms >= n
  in
  let check_linear_cstrs cstrs sol =
    List.for_all (fun cstr -> check_linear_cstr cstr sol) cstrs
  in
  check_linear_cstrs iof_and_size_cstrs.synchronizability iof_and_size_sol &&
  check_linear_cstrs iof_and_size_cstrs.precedence iof_and_size_sol &&
  check_linear_cstrs iof_and_size_cstrs.periodicity iof_and_size_sol &&
  check_linear_cstrs iof_and_size_cstrs.sufficient_indexes iof_and_size_sol &&
  check_linear_cstrs iof_and_size_cstrs.increase_indexes iof_and_size_sol