Very interesting, thank you for this writeup! Regarding the following considerations: "After a few seconds this program terminates which seems wrong. Why shou

Very interesting, thank you for this writeup! Regarding the following considerations: "After a few seconds this program terminates which seems wrong. Why should a problem that has infinitely many solutions ever terminate? Shouldn’t it run forever?" Yes, conceptually, it should of course run forever. However, at some point, even when using unbounded integers (which it, in my view, also should do), it will eventually run out of memory because the representations of involved bounds will exceed what can be stored. In such cases, from a correctness perspective, it is inadmissible to simply stop "silently", because that would be indistinguishable from cases in which there are no (further) solutions. Instead, some kind of error should be raised, indicating that it was not possible to search further than that. And when using bounded integers, likewise an error should be raised if some internal range is exceeded when searching for solutions.