Fix missing case in Boolean terms rewriting.  (Resolves bug #596.)
Merge branch '1.4.x'

Conflicts:
	src/smt/model_postprocessor.cpp
	test/regress/regress0/Makefile.am
Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).
Fix a memory leak in SatSolverRegistry (re: bug #594).
Remove some dead code.
Fixed bug in model builder with subtypes
Remove some unused variables.
Merge pull request #62 from mdeters/bv-cleanup

Remove some unused variables.
Fix bug with incremental+datatypes.  Minor cleanup.  Disable regression bug484, enable parsing_ringer.
Fix dt shared terms issue, reenable regression.
Increase stack size when running regressions (fixes some regression crashes on Mac).
Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac).
Work around an apparent bug in libc++ that was causing crashes on Mac..
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().
Update TheorySets to use CDHashSet<>::key_begin() / key_end().
Merge branch '1.4.x'
Do not eliminate variables only occurring in patterns.  Minor improvements to sort inference.  Remove unused code.
Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.
Merge pull request #63 from mdeters/theorystrings-hashset-iteration

Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().
Work on synchronizing decision=justification and E-matching.