functor (D : SMTLIBSolverDriver-> SolverSig.S