Use Error for implementation-specific contingencies only

Error is the return type of functions that must be implemented for
a specific SMT solver. Error, therefore, encourages implementations
to consider features that the underlying solver may not support.