@whitequark@mastodon.social @unlambda@hachyderm.io @regehr@mastodon.social @lenary@types.pl Okay, that makes sense. Then if it's all bounded loops, unrolling and direct SMT-LIB is almost always good enough.