Design-by-contract programming is a best practice in which a contract is used to specify the expected behavior of program elements such as functions and classes. Although enforcing compliance with these contracts at run time renders a program robust against unexpected failures, they also introduce a substantial contract monitoring overhead. Soft contract verification intends to reduce this overhead by verifying as many contracts as possible through static analysis. Thus far, the static analyses underlying existing soft contract verifiers have been based on adaptations of the AAM 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.