<p><span class="h-card" translate="no"><a href="https://infosec.exchange/@arnaugamez" class="u-url mention">@<span>arnaugamez</span></a></span> not enough experience to say</p><p>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</p><p>`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?</p>
