I actually wasn't aware of this either.
Z3 is fine with it--its job is to find any satisfying model. The possible outcomes are "the puzzle is solvable and here's a solution" or "the puzzle isn't solvable."
Z3 is fine with it--its job is to find any satisfying model. The possible outcomes are "the puzzle is solvable and here's a solution" or "the puzzle isn't solvable."
For example, in https://zayenz.se/blog/post/benchmarking-linkedin-queens/#te... I took a large number of LinkedIn Queens puzzles, and I filtered out the ones that were not well-formed so that they wouldn't mess up the benchmarking and statistics.