Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds for bounded integers.
Add --no-condense-function-values option for explicit function models (useful in some applications)
File inclusion in Smt2 parser.

The extended command (include-file "filename") now includes file content.