Add --inst-max-level=N option for Kshitij.  Support define-const command in Smt2.
Compute care graph for datatypes.  Preliminary results show 20x speed up on larger problems.  Improve datatypes rewriter.
Avoid assigning constructor terms to 1-constructor datatype eqcs, when possible, to ensure termination for codatatypes. Minor changes.