We consider the problem of reasoning over an expressive constraint language for unbounded strings. The difficulty comes from recursively defined functions such as replace, making state-of-the-art algorithms non-terminating. Our first contribution is a progressive search algorithm to not only mitigate the problem of non-terminating reasoning but also guide the search towards a minimal solution when the input formula is in fact satisfiable. We have implemented our method using the state-of-the-art Z3 framework. Importantly, we have en- abled conflict clause learning for string theory so that our solver can be used effectively in the setting of program verification. Finally, our experimental evalu- ation shows leadership in a large benchmark suite, and a first deployment for an- other benchmark suite which requires reasoning about string formulas of a class that has not been solved before.