Well, I think "obviously" was right, since my algorithm would never terminate if no source is ever found that matches the generated binary (there are infinitely many possible programs for most idealized languages).
For your idea of modifying my algorithm to bail after some number of inputs have been checked, clearly there does exist a bound on the source length necessary to generate all possible binaries of size N, since there are only finitely many such binaries (and thus they can be produced by finitely many sources). But to turn this into an algorithm, you'd need a computable bound. For a language like C, I think such a bound probably exists and is a reasonable function of the input size. For a language like Coq, though, I doubt the bound would be computable. Basically, I think that there are programs that work for reasons that are very difficult to prove.
Also, I think we're far enough from practical that appeals to the real world are somewhat silly. Either we're interested in understanding the theoretical situation, in which case lack of real world examples doesn't help, or we're interested in practical decompilation, in which case this whole conversation is stupid.