DISCLAIMER: I had originally posted this to CS.SE, but I've deleted it and moved it here, since it received little attention, and I think it is a research level question.
According to this paper, if there is a solution to a quantifier free Presburger formula, there is a solution whose size in bits is polynomial in the problem size. This allows the problem to be in $NP$, easier than arbitrary Presburger formulas.
However, the paper doesn't explicitly reference where this bound comes from, just mentioning a connection to Integer Linear Programming.
I was wondering if anyone knew, what was the exact bound on the solution size, or if they could provide a reference for such? I have another problem which I can phrase as a QF Presburger formula, and I'd like to find a definite bound on the solution size. But I'm also trying to work it into an actual software system, so simply knowing "there exists a polynomial" doesn't help me much.