Another build fix; the dust should be settled now.
Some patches to CVC3 compatibility layer; Thanks to Adam Buchbinder @ Google for the report and patch!
Add virtual destructors where missing
Datatype::getCardinality() caching
Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google for the report and patch!
Allow empty record literals (fixing an oversight in previous work on empty tuples/records)
Minor fixes for Mac OS Mavericks
Add fair strategy for finite model finding multiple sorts --uf-ss-fair.
Bug fix for previous commit
Changing the number of bits allocated per field in node values.
Adding the changes needed to delete rewriter attributes.  This includes being able to list attributes.  Additionally, added debugging hooks to node manager and attribute manager.
Array collectModelInfo fix for Andy
Substantial Changes:

-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default.  This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.

- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.

- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.

Minor Changes:

- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.

- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
Merge remote-tracking branch 'CVC4root/master'
Minor fix for swig bindings.
Fix Java destruction order issue; thanks to Zheng Manchun for reporting this bug.
Fix Java output stream adapter.
Fix C++-to-Java exception translation.
Fix a segfault in the printer infrastructure when called from API and no language is set
Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter