Quanitifier Free Presburger Arithmetic: Upper bound on solution size?
You can find an answer in the following paper:

Joachim von zur Gathen, Malte Sieveking. A bound on solutions of integer linear equalities and inequalities.
Proc. AMS 72(1) (1978)
(pdf)

A simple corollary of their result follows.
Let's say we have two integer systems, $A x = b$ and $C x \ge d$,
where you want $x$ to be in $\mathbb Z^n$.
Consider determinants of all square submatrices of the matrix $E = \left(\matrix{A &amp; b \\ C &amp; d}\right)$
and denote by $M$ an upper bound on their absolute values.
(In other words, set $M$ to be larger than or equal to the absolute value of all minors of $E$.)
Now, if there exists an $x \in \mathbb Z^n$ satisfying both $A x = b$ and $C x \ge d$, then
there exists such an $x$ whose components are at most $(n + 1) M$ in absolute value.

It remains to note that a determinant of a $k \times k$-matrix $S$ is at most $k!\, \|S\|_{\mathsf{max}}^k$
where $\|S\|_{\mathsf{max}} = \max |s_{i j}|$. Combining these two bounds will give a specific polynomial
bound on the size of a smallest solution (and this is already an easy exercise).