Fix tokenization of "reset" in SMT-LIB v2.0.  It's a reserved word only in 2.5.
Fix BV inequality solver caching.
BV inequality graph TNode fix.
Merge pull request #65 from mdeters/bv-ineq-cachefix

Fix BV inequality solver caching, and TNode fix.
Possible fix for bug594
More preparation for filtering relevant terms in TermDb.
Remove two obsolete versions of MBQI.
Merge pull request #69 from mdeters/bug594

Fix memory leak in CDHashMap<> with Node keys (resolves bug 594).
Copyright text fixes.
Minor adjustments to wording.
Minor changes to AUTHORS and COPYING
Be lazier to consider EQC in UF+cardinality solver.  Minor cleanup.
Add term db mode.  Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches.  Minor cleanup.
Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
New, uniform checkTime statistic for all theories (as discussed in meeting).
Short-circuit in TheoryArithPrivate::check(), care of Tim.
added command line option for extractArith bv rewrite
Add local theory extensions instantiation strategy (incomplete).  Refactor how default options are set for quantifiers.  Minor improvement to datatypes.  Add unsat co-datatype regression.  Clean up instantiation engine.  Set inst level 0 on introduced constants for types with no ground terms.  Return introduced constant for variable trigger when no ground terms exist.
Compute model basis only for fmf.  Add another co-datatype regression.
All Minisat solve calls now return lbool (fixes bug 599)