<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> ah, I don't know then. I've not used the C bindings much, but Nuno preferred them over the C++ bindings for Alive2, despite the fact that Alive2 is in C++. I forgot the reason.</p><p>you could emit SMT-LIB. I don't know. in Souper that's what we did and it's really slow, but a superoptimizer is making lot more solver calls than you're looking at.</p>
