Design-by-technique for CESK machines. Intended solely to introduce the concept of soft contract verification, these purpose-built analyses lack configurability. In this paper, we propose a novel static analysis for soft contract verification called abstract concolic execution. We systematically abstract a concolic execution, which is a form of dynamic symbolic execution, into abstract concolic execution, rendering the technique terminating and sound for any program input. To show that our analysis is more configurable than the state-of-the-art analysis supporting soft contract verification, we propose two variations of the analysis. Finally, we show that our approach is comparable to if not more precise than the state of the art at the cost of performance. We find that in 10 out of the 24 benchmark programs, our approach is more precise than the state-of-the-art approach, while being as precise in 9 of them and less precise in 5.