Why do all recent SAT solvers work on CNF instead of circuit SAT?

Question

After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG tracks. However since then it seems the focus has been entirely on either SMT or improving clausal SAT solvers.

Intuitively to me concentrating on circuit SAT seems to make a lot of sense: Many if not most problems are more naturally expressed as circuit SAT than CNF; circuits provide structural information that cannot be reverse engineered from CNF, but circuits can always be transformed into CNF; and at least the industrially significant field of logic synthesis seems to be a particularly good fit for AIGs.

So, what happened? Did it turn out that the extra structural information does not help solvers? Was AIG-based SAT solving a failed experiment?