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.
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.
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.