Hire me!!!!!!!!

hireme.ipynb

It seems like you are incorrectly excluding a model from the solver. Instead of:

solver.add([i!=model[i] for i in inp])

it should be:

solver.add(Or(
  [inp[i] != model[inp[i]] for i in range(0, 32)]
))

See this gist for an example.

By doing this incorrectly you're overly limiting the number of input candidates generated by Z3 solver. That is - you're not guaranteed that the solver will generate any input candidate, that could be used (in solve_round) to calculate the solution. I guess, in example above, you were able to get the solution, because fortunately the valid input candidate had not been eliminated, before it was generated (and used). I wonder if you've tried target strings other than "Hire me!!!!!!!!\x00"? Like "LiveOverflow!!!\x00", that you mention in the comment.

FYI: I don't have sage installed, so I haven't run the code in its entirety. But I've run the 'Z3 model exclusion' part, like you can see in a gist linked above.