Consider a system of equations of the form $x y = z$ where the variables $x,y,z$ are taken from a common vector $\overline{t} = \overline{a} + \sum_{i = 1} \lambda_i \overline{b_i}$ where $\overline{a}, \overline{b_i} \in \mathbb{N}^k$ and $\lambda_i \in \mathbb{N}$.
Is there an algorithmic way of checking whether the system has a solution?
This problem is undecidable by a reduction from solvability of Diophantine equations (Hilbert’s 10th problem).
By introduction of new variables corresponding to subexpressions of a given polynomial, we can efficiently reduce the solvability of any integer polynomial system to solvability (over $\mathbb N$) of a system $S\cup P$, where $S$ consists of equations of the form $x_i+x_j=x_k$ or $x_i=1$, and $P$ of equations of the form $x_ix_j=x_k$. The solution set of $S$ is definable in Presburger arithmetic, and therefore semilinear, thus it can be (algorithmically) written as a finite union $S=\bigcup_jS_j$ where each $S_j$ has the form $\vec a+\sum_i\lambda_i\vec b_i$ as in the question. Then the original system is solvable iff for some $j$, $P$ has a solution in $S_j$.
