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;