<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> yeah, awesome. one way is to use Z3 as a library, another is to emit SMT-LIB, which is a bit of a pain but then you get process separation from the solver (giving reliable timeouts for ex) and also you can use another solver, such as CVC5</p>