@arnaugamez not enough experience to say
Z3 commits crimes, with one of the biggest ones is the pervasive use of semantically unforgivable operator overloading and silent truncation in the Python interface
`a >> b` you might think this works the same for bit vectors as it does for Python integers, but Z3 uses arithmetic right shift for it. guess who just lost like 8 hours to this?