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)

adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real

updated generated file;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;