  We introduce a model-complete theory which completely axiomatizes the
structure $Z_{\alpha}=(Z, +, 0, 1, f)$ where $f : x \to \lfloor{\alpha} x
\rfloor $ is a unary function with $\alpha$ a fixed transcendental number. When
$\alpha$ is computable, our theory is recursively enumerable, and hence
decidable as a result of completeness. Therefore, this result fits into the
more general theme of adding traces of multiplication to integers without
losing decidability.
