Scanning http://www.hackersdelight.org/aha/aha.pdf, it looks like Aha performs some form of exhaustive search over all programs? An SMT solver is probably a better way of doing this search; there's been some work in this direction.

Jha, Gulwani and colleagues have a very nice paper on oracle-guided synthesis. They show how you can generate loop-free bitvector programs using SMT: http://www.eecs.berkeley.edu/~sseshia/pubdir/synth-icse10.pd.... John Regehr has also written about this on his blog: http://blog.regehr.org/archives/1146.

Part of the complexity here in an SMT solution might be encoding all the bizarre instructions that you could possibly take advantage of in x86-like instruction sets.