It is well known that for general linear loops of the form
involving a nondeterministic choice over guarded linear assignments, termination is undecidable when the conditions
while A do B_1 -> v := C_1 v + d_1 | ... | B_n -> v := C_n v + d_n od
A, B_1, ... , B_ncan 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.