Decidability of diophantine equations over {=, +, gcd} It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $\{=, +, \cdot, 1\}$ (of equality, addition, multiplication, and the constant $1$), with free variables taking values in the integers, deciding whether the formula is satisfiable is undecidable.
If multiplication $\cdot$ is replaced by the binary greatest-common-divisor (gcd) function, defined appropriately for 0 and negative numbers, does the satisfiability problem remain undecidable?

For example, the input might be a formula like
$$
a + b = c \land \gcd(a, b) = 2 \land \gcd(a, c) = 1
$$
or
$$
\gcd(a, \gcd(b, c) + b) = a + c \land \lnot (\gcd(a, b) = a).
$$
I suspect this to be a basic result in the study of decidability results for integer theories, but this came up in another context and I am not entirely familiar. From a brief literature search (see On Decidability Within the Arithmetic of Addition and Divisibility, Marius Bozga and Radu Iosif) I know of the following classical results:

The theory of $\{=, +, |\}$ (where $|$ is divisibility) allowing quantifiers is undecidable (Julia Robinson 1949).

The satisfiability of quantifier-free formulas over $\{=, +, |\}$ (i.e. existential fragment of the above) is decidable. (The diophantine problem for addition and divisibility, Leonard Lipshitz 1976.)


Divisibility can be defined in terms of gcd ($a \mid b \iff \gcd(a, b) = a$), but vice versa requires existential quantification ($\gcd(a, b) = c \iff (c \mid a) \land (c \mid b) \land \exists x \exists y.\; c = ax + by$), which won't work in quantifier-free formulas in a negated context, so at least at first glance I am not sure that gcd is equivalent to divisibility for the purposes of decidability.
($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$, and $\le$:
$$\begin{align*}
\gcd(a,b)=c&amp;\iff c\ge0\land c\mid a\land c\mid b\land\forall d\:(d\mid a\land d\mid b\to d\mid c)\\
&amp;\iff c\ge0\land c\mid a\land c\mid b\land\exists u,v\:(a\mid u\land b\mid v\land c=u+v).
\end{align*}$$
Thus, any existential sentence over the structure $\langle\mathbb Z,+,\gcd\rangle$ (or even $\langle\mathbb Z,{\le},+,\gcd\rangle$) can be (in polynomial time) converted to an equivalent existential sentence over the structure $\langle\mathbb Z,{\le},+,|\rangle$, which can in turn be converted to an equivalent existential sentence over the structure $\langle\mathbb N,+,|\rangle$ in the obvious way. The last problem is decidable by the result of Lipshitz [1] quoted in the question.
Reference:
[1] Leonard Lipshitz: The Diophantine problem for addition and divisibility, Transactions of the American Mathematical Society 235 (1978), pp. 271–283, doi: 10.1090/S0002-9947-1978-0469886-1.