fixing bug580 caused by bad bv inequality explanation
Do not use pure theory terms as single triggers.  Minor cleanup.
Set instantiation level on skolemized bodies of quantifiers.  Rename inst-level attribute to quant-inst-max-level
Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation.  Print --dump-instantiations on sat/unknown.
Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering.
check() optimization

Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
Merge remote-tracking branch 'origin/master'
Update command_executor_portfolio.cpp
Accept user-provided triggers with variable terms.  Flush lemmas before quantifiers check.  Minor fix for conjecture generation.
Fix bug for variable term triggers within multi-triggers.
sets stronger equality propagator