make timeout part of the SMT filter's tail

merge

split "smt_filter" into head and tail

fewer facts to SInE-E

Z3 sometimes reports two errors, with the first one referring to line 1 for some strange reason -- but it makes no sense to kill line 1, so we traverse the errors in reverse and consider only the last error

trap one more Z3 error

fixed the command-line syntax for setting Yices' random seed

merged

updated SMT certificates

fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order; fixed introduction of explicit application: use explicit application for every additional argument (grouping of arguments caused confusion when translating into the intermediate format)