It is well known that for general linear loops of the form
while A do
B_1 -> v := C_1 v + d_1 | ... | B_n -> v := C_n v + d_n
od
involving a nondeterministic choice over guarded linear assignments, termination is undecidable when the conditions A, B_1, ... , B_n
can be arbitrary linear constraints. Interestingly, requiring them to be conjunctions of linear equations is enough to make the problem decidable. I will show a proof of this which uses surprisingly elementary methods.