I've done some very, very preliminary work to pave the way towards iteration and recursion in superoptimizers, but you are correct that "straight-line over tiny

I've done some very, very preliminary work to pave the way towards iteration and recursion in superoptimizers, but you are correct that "straight-line over tiny problems" is mostly where it's at. Even multiplication ops are a real bear for SMT. I can get them to work, but they are way more expensive than other arithmetic. From what I understand, the whole 'approximate with uninterpreted functions' stuff can be done under the hood by SMT solvers during bit-blasting - from what I understand, more expensive operations can be expanded lazily (and until then treated as UFs) in the hope that useful properties emerge. Logics that have floating point theories do exist in the SMT benchmarks but like a big coward I haven't played with them. You can't entirely ignore cost issues in a superoptimizer - the difference between, say, a latency = 3 instruction like a multiply and a latency = 1 operation might be decisive. But (a) there are ways to model this in your optimization process and (b) fine differences of cost aren't the primary issue when superoptimizing anyhow. The later point is decisive - I have a benchmark (on bytewise set membership) in my superoptimizer where I example 25 million 4-instruction specializations and there are only 7 solutions. I think I can spend a few extra cycles evaluating with of those 7 will be faster under a range of transforms, etc etc - the expensive part was finding 7/25M solutions to begin with (or, as is often the case, finding 0/25M solutions).