Presburger arithmetic and finite model property

Question

I'm learning about model theory and first order logic. Recently, I read about finite model property and Presburger arithmetic, and I have two questions about them:

1. Does Presburger arithmetic has finite model property?

2. Given a Presburger formula. Clearly, it is SAT. Does it have finite number of models?

$$ \forall x.~ x>0 ~\wedge ~ y \ge 0 ~ \wedge ~ z \ge 0 ~ \wedge ~ x=y+z $$