Bug fixes for --purify-triggers, --dt-force-assignment.
Improved SMT-LIBv2 language support for unsat cores.
Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.
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'