<p><span class="h-card" translate="no"><a href="https://mastodon.social/@whitequark" class="u-url mention">@<span>whitequark</span></a></span> at the SMT query level, it should be pretty reasonable, you're basically saying "give me a model where the target displays a behavior not shown by the source" and then if this is unsat you're good</p>
