Can top SAT-solvers factor easy numbers?
There are other much simpler instances which we provably know that the current algorithms cannot solve in sub-exponential time. These algorithms are incapable of counting (almost all of them are improvements of DPLL which correspond to Resolution propositional proof system).
Unfortunately such examples are unsatisfiable instances. The question about finding  natural satisfiable hard instances for these algorithms is an interesting research problem (Russell Impagliazzo mentioned this during the proof complexity workshop last year at Banff). There are satisfiable instances that we provably know the algorithms fail badly if there is any such instance, but they are not very natural (they are based on formulas expressing the soundness of algorithms).
Regarding factoring, if the size of numbers are small (e.g. logarithmic as in your case, i.e. the numbers are given in unary), then theoretically there is no result that says there cannot be solved by current algorithms, and in fact we can write simple polynomial time algorithms that factor these numbers. So whether a particular SAT solver program can solve them might depend on the particular algorithm.