I don't think it specifically states that this is z3-python (not a nitpick) which has an added bonus in that you can handle the SSA requirements if you're allocating inside a finite loop in the higher level language.
I was stuck on that at one time in the past, and then realized that not all the python code is in the scope of the solver and hence helps you automate those state additions.
Comments
Nice article!!
I don't think it specifically states that this is z3-python (not a nitpick) which has an added bonus in that you can handle the SSA requirements if you're allocating inside a finite loop in the higher level language.
I was stuck on that at one time in the past, and then realized that not all the python code is in the scope of the solver and hence helps you automate those state additions.
These techniques aren't purely academic either, I've used them for reverse-engineering malware and software vulnerability analysis e.g. this inversion of MurmurHash3 https://www.josephkirwin.com/2018/04/07/z3-hash-inversions/