* 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, 6 insertions, 0 deletions

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 77274d575..eb7b56b19 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -24,6 +24,7 @@
 #include <signal.h>
 
 #include "util/exception.h"
+#include "util/Assert.h"
 
 #include "cvc4autoconfig.h"
 #include "main.h"
@@ -75,6 +76,11 @@ void cvc4unexpected() {
           "\n"
           "CVC4 threw an \"unexpected\" exception (one that wasn't properly specified\n"
           "in the throws() specifier for the throwing function).\n\n");
+  if(CVC4::s_debugAssertionFailure == NULL) {
+    fprintf(stderr, "The exception is unknown.\n\n");
+  } else {
+    fprintf(stderr, "The exception is:\n%s\n\n", CVC4::s_debugAssertionFailure);
+  }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
     set_terminate(default_terminator);