It is well-known that if an integer linear program has a feasible solution, then it has a feasible solution whose bit size is polynomially bounded. For example, here is Theorem 13.4 from Papadimitriou and Steiglitz' Combinatorial Optimization book (paraphrased):
Consider the ILP $$Ax \le b, \quad x \ge 0, \quad x \in \mathbb Z^n,$$ where $A$ is an $m\times n$ matrix. Let $r = \max |a_{ij}|$ be the largest value appearing in $A$, and let $s = \max |b_j|$. Then if the ILP has a feasible solution, then it has a feasible solution $x$ with $x_i \le (n+m)(mr)^{2m+3}(1+s)$ for each $i \in [n]$.
Via binary encoding, this implies that integer programming is contained in NP. (The intuition is that large coefficients are required to induce sharp angles in the polyhedron. Results like above can be found in many textbooks, but the following question never seems to be addressed.)
I wonder whether the upper bound given is actually attained. Are there examples of feasible integer programs where all coefficients are small (maybe even $|a_{ij}|, |b_j| \le 1$) and yet all feasible solutions contain exponentially large numbers?
Equivalently, I wonder whether feasible integer programs encoded in unary have a solution whose unary size is polynomially bounded in the input size.