MainSolver requires concrete SMTConfig because it eagerly constructs SimpSMTSolver that requires parameters.
This is certainly inconsistent with the fact that Opensmt is possible to construct without SMTConfig, allowing to modify some parts of the config later, but not all.
MainSolver should be possible to construct lazily once it is required. Similarly, the construction of SimpSMTSolver inside of MainSolver may be lazy as well.
This may be connected to #666 (hmm is 666 just a coincidence here? :fearful:)
MainSolverrequires concreteSMTConfigbecause it eagerly constructsSimpSMTSolverthat requires parameters. This is certainly inconsistent with the fact thatOpensmtis possible to construct withoutSMTConfig, allowing to modify some parts of the config later, but not all.MainSolvershould be possible to construct lazily once it is required. Similarly, the construction ofSimpSMTSolverinside ofMainSolvermay be lazy as well.This may be connected to #666 (hmm is 666 just a coincidence here? :fearful:)