pretty name for ==>

added HOL-Boogie

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

ignore parsing errors, return empty assignment instead

scheduler: clarified interrupt attributes and handling;

worker_next: plain signalling via work_available only, not scheduler_event; scheduler: tuned worker pool adjustments;