Some fixes to symmetry breaker (resolves bug 576).
fixed bug575 for bv models
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
Making getEqualityStatus more powerful for bit-vector theory.
Produce error for bad indexed function names in SMT-LIB, remove antlr warning.
Merge branch '1.4.x'
Add option for inductive strengthening based on well-founded induction for integers (default schema).
Update bv proof signature and example, after discussions with Liana.
Fix --inst-max-level for strategies that use arbitrary representative terms.
Avoid doing work in quantifiers engine when no quantifiers are asserted.
Fix SMT1 parser :extrasorts/:extrapreds.
Fix operator-printing issue in SMT2.