avoid slightly odd Conv.tap_thy

allocate intermediate directories in module hierarchy

export experimental options

merged

compile

run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers

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)

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;

tuned signature;

clarified exports of structure Simplifier;

refer to regular structure Simplifier;

tuned;

updated SMT certificates

more precise/correct SMT error handling

fixed off-by-one and return proper error code -- never underestimate the number of oddities in Perl

discriminate SMT errors a bit better

keep track of errors in Z3 input file for debugging purposes

better propagation of stdout in case of failure + comply with strict/warnings