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;

revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);

avoid broadcast work_available, use daisy-chained signal instead; max_threads: allow as much as 4 * m, after extra delay;

fulfill_proof_future: tuned important special case of singleton promise;

worker_next: treat wait for work_available as Sleeping, not Waiting; max_threads: simple adaptive scheme between m and 2 * m;

worker activity: distinguish between waiting (formerly active) and sleeping; tuned;

tuned;

tuned thread data;

worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock); worker_start: back to non-self version; scheduler: status output based on ticks;

slightly leaner and more direct control of worker activity etc.;