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