Minor fixes post-merge of RR.
Work on array pf signature, add working example.  Add quantifiers proof signature. Ignore terms not in current master EE for QCF.  Minor refactoring.  Make --rewrite-rules true by default.
Add working example of LFSC proof with quantifiers.  Update quantifiers signature to avoid dependent types in side condition.
New --tear-down-incremental mode, useful for debugging and performance profiling.
Better approach to forcing string logics to contain UFLIA also.
proof signatures makefile