<p><span class="h-card" translate="no"><a href="https://mastodon.social/@whitequark" class="u-url mention">@<span>whitequark</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@lenary" class="u-url mention">@<span>lenary</span></a></span> <span class="h-card" translate="no"><a href="https://hachyderm.io/@unlambda" class="u-url mention">@<span>unlambda</span></a></span> if your compiler is in Python, the Z3 python bindings are super nice. also there are CVC5 bindings that supposedly are mostly compatible, but I've never bothered to try that out. </p><p>emitting SMT-LIB adds an annoying level of indirection through strings, that's probably not the way I'd go if your language has good Z3 bindings</p>
