added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
replaced unspecific 'error' invocations with raising of specific SMT exceptions,
added annotations to traced SMT problem and solver output
(benchmark Isabelle
:extrasorts ( T1)
:extrapreds (
(up_1)
)
:assumption (not (iff (and up_1 true) up_1))
:formula true
)