New module for generating candidate equality conjectures used in inductive proofs.  Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness.  Refactoring of term database.  QcfEngine now uses central data structure for term indexing.  Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).
Minor cleanup from previous commit.  Better organization for how quantifiers modules check (introduce QuantifiersEngine::QEffort).
Better support for resource-limiting when there aren't any actual conflicts.
Some fixes to symmetry breaker (resolves bug 576).
Some fixes to symmetry breaker (resolves bug 576).
Minor fix : do not drop instantiation patterns when merging quantifiers.
fixed bug575 for bv models
fixed bug575 for bv models
Fix for manpages.
First crack at fixing double-linking issues in build system.
Fix double-linking issue (I think) by simplifying builds/ structure.
Fix win32 build.
Another build fix.
Add draft of BV proof signature (incomplete) and example proof.
Fix a build issue for some configurations, thanks Tianyi.
To avoid confusion, permit --enable-staticbinary as an alias for --enable-static-binary.
Update smt_engine.cpp

Code changed but comment didn't, might as well get rid of it.
Add support for quantifier-specific instantiation levels.  Add option for setting inst-level 0 only for input terms.
Revert a8e0ce67 and add test case (resolves bug #578).

This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.
Merge branch '1.4.x'

Conflicts:
	test/regress/regress0/Makefile.am