z3 says: sat  counterexample x = -1431655766  x*3 wraps to -2  and divides to -1
with the guard (x*3 must not wrap) the split proves it, as chapter 11 shows.
