BoolExpr removed and replaced with Expr
Bug-related:

* ITE removal fixed to be context-dependent (on UserContext).
  Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
  (partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
  was labeled sat); re-enable it for "make regress"

Also:

* --check-model doesn't fail if quantified assertions don't simplify away.

* fix some examples, and the Java system test, for the disappearance of the
  BoolExpr class

* add copy constructor to array type enumerator (the type enumerator
  framework requires copy ctors, and the automatically-generated copy ctor
  was copying pointers that were then deleted, leaving dangling pointers in
  the copy and causing segfaults)

* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
  you to dump before/after a particular preprocessing pass.  E.g.,
  --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
  "--dump=assertions" by itself is after all preprocessing, just before CNF
  conversion.
* minor fixes to dumping output
* include Model in language bindings

Minor refactoring/misc:

* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
  (e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
  options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications
fix \file
* Fix some regressions' expected outputs.

* Ensure Rewriter::init() is called before ::rewrite().
  The array type enumerator recently gave us an end-run around
  ::init().  TheoryEngine no longer calls these, they're done
  via static initialization.

* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).

(this commit was certified error- and warning-free by the test-and-commit script.)
* Include a few bug testcases for resolved bugs.

* Fix error message if you POP beyond the bottom user stack frame.

(this commit was certified error- and warning-free by the test-and-commit script.)
* Some documentation about building compatibility and language bindings
* Better errors/warnings when SWIG isn't installed (resolves bug 373)
* Allow compatibility bindings to be built when SWIG isn't available
* Clean up some options documentation
* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation

(this commit was certified error- and warning-free by the test-and-commit script.)
* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASS
* more minor cleanup/doc

(this commit was certified error- and warning-free by the test-and-commit script.)
turn off cudd by default in configure script
fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't allow use of any BV ops
small fix for compat JNI library installation
Fixed problem in assertEqualityEngine: predicates that are not false are no
longer assumed to be true
added reduced bv model failing test case
* Models' SubstitutionMaps are now attached to the user context
  (rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes

(this commit was certified error- and warning-free by the test-and-commit script.)
adding mergePredicates method to the equality engine to be able to
assert equalities betweeen predicates 
some documentation fixes
fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 417.  oops.  also fix spelling on "rewritting" test
* Add assertion in TheoryModel code to ensure we don't get inconsistent
  substitutions for solved variables.  Related to bug 418 (and might
  resolve it).

* Respect phase-locking in Minisat (one phase-saving site was unguarded).

(this commit was certified error- and warning-free by the test-and-commit script.)
fix for bug 415
usability: remove --no-interactive from --smtlib option