Added new, much faster, care graph computation for arrays
Force split on true first in combineTheories
Fix bugs in getModelValue in bit-vectors
Be more lazy about generating array lemmas
Do not allow duplication of function definitions.  Set incomplete flag in model builder.
Fix some mistakes in datatypes theory combination, disable two regressions.  Minor fix for fun defs.
Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being rewritten).  Minor improvement to dt care graph.  Reenable regressions.
Simplify which lemmas to communicate in dt.
Fix cegqi for synthesis without syntax.
Added cache to getModelValue
More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind.  Minor fixes for fun_def_process.  Other minor changes.
Fix get-bug-attachments script.
Merge branch '1.4.x'