Game Constraints with Z3