Fix unit test (compile error) for new SatSolver interface
Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory
fixed getModelValue to only query the value of leaves and evaluate more complex bv terms
Added check for infinite lemma loop
Fixes for getModelVal in bv theory
Improved speed of no redundant lemma assertion by using hash set
flatten or nodes
generalize to handle and
boolean flatten rewrite: dont re-rewrite
boolean flatten: bug fix in dfs search

(this is not intended to (and doesn't) address the issue with
NodeBuilder limit)
bool flatten: node num_children workaround
fixing destruction order in SmtEngine
making sure sat context is zero when user context is popped to 0 in SmtEngine destructor
add bit0 and bit1 constants to smt-lib v1 parser
Theory "alternates" support

* This is a feature that Dejan and I want for the upcoming tutorial.
  It allows rapid prototyping of new decision procedure implementations
  (which we may choose to demonstrate), and a new --use-theory command-line
  option to select from different available implementations.  It has no
  affect on the current set of theories, as no "alternates" are defined.

* Also update the new-theory script, which was broken and incomplete.