* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 2a1b1d0fc..eed542e8a 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -222,7 +222,8 @@ throw(OptionException) {
       opts->strictParsing = true;
       break;
 
-    case DEFAULT_EXPR_DEPTH: {
+    case DEFAULT_EXPR_DEPTH:
+      {
         int depth = atoi(optarg);
         Debug.getStream() << Expr::setdepth(depth);
         Trace.getStream() << Expr::setdepth(depth);