Ultimately there is no real computer that is Turing complete, because all real computers are finite. Ultimately, you can represent any real computer with a (ve

Ultimately there is no real computer that is Turing complete, because all real computers are finite. Ultimately, you can represent any real computer with a (very large) DFA. The two things missing from what would normally be considered a universal computer are conditionals and indirect addressing. The Z3 is also limited in that it executes a specific finite set of instructions in linear order, with no branching. In the proof, they get around the finite length of a program by literally creating a loop -- they glue one end of the paper tape of the program to the other so that the computer can keep executing the same instruction stream forever. Then they get around the lack of indirect addressing by accessing every memory location in every loop. I agree that it's very much a stretch to call the Z3 Turing complete.