Recent progress in solvers modulo theories reach a point where it seems feasible to perform automatic static analysis of whole programs (and not just paths) using solvers. We will discuss the expected advantages and drawbacks of such approaches based on first-order logic domains, and provide semantic foundations to discuss their soundness. If time permits, we will also show the links between the reduction process used in abstract interpretation and the Nelson-Oppen decision procedure. The ultimate goal will be to use such links to combine logical abstract domains using solvers and more ad-hoc abstract domains in order to get the best of both approaches in one analyzer.