Model output is now const; this related to bug 519
add relevant domain computation
Fix for bug 519; don't involve ITESimplifier in model generation.
Fix for Boolean-term rewriting and LAMBDAs
Support for TPTP's TFF0 (with arithmetic)

This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).

This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made.  These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
Remove auto-aritization from TPTP parser
Fix for curious GCC 4.8 translation with -O.
Fix language bindings and portfolio builds.
Remove now-unused language bindings interface file.
Minor bugfixes to model-building
"Tabular"-style function definitions in models with --no-condense-function-values
Fix for get-antlr script and PIC/non-PIC objects, on some platforms
fixed bug520
fixed seg fault when bv equality is turned off
Fix bug 516; include some bug testcases.
Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine.
Minor fix for --no-condense-function-values
possible fix for bug 521
enable bug521 regression tests
Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.