Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.
Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
SMT-LIB printer updates (some missing cases).
Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.
Merge branch '1.2.x'
Updated CASC scripts, as provided to Geoff Sutcliffe
Merge tag 'casc24'
Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds for bounded integers.
Fix clang static initialization order issue; fixes bug 512.
Merge branch '1.2.x'
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.
Fix bug in --fmf-fmc for producing models of functions not appearing in quantified formulas.
IDL example theory (to be used with --use-theory=idl).
typo
small parese issue in IDL
Allow disabling include-file feature
Fix for bug 517.
One more case for arrays of Boolean.
Fix typos in alttheoryskel