Solving the Whole Year Puzzle with Z3