<p><span class="h-card" translate="no"><a href="https://mastodon.scot/@rasteri" class="u-url mention">@<span>rasteri</span></a></span> <span class="h-card" translate="no"><a href="https://infosec.exchange/@arnaugamez" class="u-url mention">@<span>arnaugamez</span></a></span> you can do it in a reasonable manner; Amaranth for example overloads Python operators _and gives them Python semantics_</p><p>Z3 does not do it in a reasonable manner</p>