Consider adding infrastructure to check if term is from a solver

[makaimann]

Could include the solver in every term which would allow term construction without a separate solver object. But this could be expensive. Another option is to just have an interface for asking a term if it belongs to a solver. Depending on underlying solver, could depend on its API instead of using smt switch objects