Minor fix for --user-pat=resort
Improve stats in conjecture generator, minor cleanup.
Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.
Preprocessing step for finding finite runs of well-defined function definitions using FMF.
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
sygus input language and benchmark