The paper goes on to say that > Unfortunately, in practice it would seem that SMT solvers are monolithic, and SMT internals expertise is required for implement

The paper goes on to say that > Unfortunately, in practice it would seem that SMT solvers are monolithic, and SMT internals expertise is required for implementing new theory solvers. and > We argue that programmers should not have to be SMT internals experts in order to implement theory solvers for their domain of interest. We propose to evaluate that claim by developing a framework for implementing custom, efficient domain-specific solvers. In doing so, we hope to democratize theory solver development and make it accessible to programmers who are not SMT internals experts, in the same way that Delite aimed to democratize DSL implementation and make it accessible to programmers who are not compiler experts. The title should give a hint. ;)