def solver(self, timeout=None):
return Z3StrProxy(timeout=timeout)<EOL>
This function should return an instance of whatever object handles
solving for this backend. For example, in Z3, this would be z3.Solver().