Some parts of this are true, but bringing up z3 is kind of a random tangent without any actual knowledge to be shared behind it.