Fixes for Boolean terms in arrays (including fix for bug 517).
Fix in SMT2 parser for parametric datatypes
Make --var-elim-quant true by default.  Add rewrite engine to quantifiers module.
Java streams example I forgot to add a long time ago
Give a more useful parse error message for "undeclared variable -1".

Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small
change to the parser to detect when something like "-1" is used but
undeclared, and adds a note to the error message giving the syntax for
unary minus.
Fix to the "include" extended feature of the SMT-LIB parser
Workaround for suspected clang 3.0 codegen bug on Mac
Merge branch '1.2.x'
Fix failure in non-assertion builds on incorrect SmtEngine use.
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.
Add files missing from last commit
Refactoring of model engine to separate individual implementations of model builder.  Begin work on interval models for integers.  Other minor cleanup.
Proposed fix for bug #513
Merge branch '1.2.x'
Add support for interval models in bounded integers MBQI (in progress).
Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Better user documentation for mkVar() and mkBoundVar().

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape to user space

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Small fix for IS_INTEGER.