-
-
Save LiveOverflow/683181b72b4123fdb325956d6f038e72 to your computer and use it in GitHub Desktop.
Nevermind, it works now. There was a bug in my installation. Some obvious features were working incorrectly. Reinstalled in a new environment and now it works.
Thanks!
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.
Sure. What I mean is that, the solver never gets to the "SOLVED" stage. I get the following output
It also means that in the recursion step in
solve_round, it never gets aTruevalue forresas there is no output that is beginning with inp.Also I am running SageMath 9.0 with a Python3.7 backend.