1 files changed, 0 insertions, 171 deletions
diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
deleted file mode 100644
index 1150f41f1..000000000
--- a/src/base/cvc4_assert.cpp
+++ /dev/null
@@ -1,171 +0,0 @@
-/*********************                                                        */
-/*! \file cvc4_assert.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Chad Brewbaker
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Assertion utility classes, functions, and exceptions.
- **
- ** Assertion utility classes, functions, and exceptions.  Implementation.
- **/
-
-#include <new>
-#include <cstdarg>
-#include <cstdio>
-
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-#ifdef CVC4_DEBUG
-//thread_local const char* s_debugLastException = NULL;
-#endif /* CVC4_DEBUG */
-
-
-void AssertionException::construct(const char* header, const char* extra,
-                                   const char* function, const char* file,
-                                   unsigned line, const char* fmt,
-                                   va_list args) {
-  // try building the exception msg with a smallish buffer first,
-  // then with a larger one if sprintf tells us to.
-  int n = 512;
-  char* buf;
-  buf = new char[n];
-
-  for(;;) {
- 
-    int size;
-    if(extra == NULL) {
-      size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
-                      header, function, file, line);
-    } else {
-      size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n  %s\n",
-                      header, function, file, line, extra);
-    }
-
-    if(size < n) {
-      va_list args_copy;
-      va_copy(args_copy, args);
-      size += vsnprintf(buf + size, n - size, fmt, args_copy);
-      va_end(args_copy);
-
-      if(size < n) {
-        break;
-      }
-    }
-
-    if(size >= n) {
-      // try again with a buffer that's large enough
-      n = size + 1;
-      delete [] buf;
-      buf = new char[n];
-    }
-  }
-
-  setMessage(string(buf));
-
-#ifdef CVC4_DEBUG
-  LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
-  if(buffer != NULL){
-    if(buffer->getContents() == NULL) {
-      buffer->setContents(buf);
-    }
-  }
-#endif /* CVC4_DEBUG */
-  delete [] buf;
-}
-
-void AssertionException::construct(const char* header, const char* extra,
-                                   const char* function, const char* file,
-                                   unsigned line) {
-  // try building the exception msg with a smallish buffer first,
-  // then with a larger one if sprintf tells us to.
-  int n = 256;
-  char* buf;
-
-  for(;;) {
-    buf = new char[n];
-
-    int size;
-    if(extra == NULL) {
-      size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
-                      header, function, file, line);
-    } else {
-      size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n  %s\n",
-                      header, function, file, line, extra);
-    }
-
-    if(size < n) {
-      break;
-    } else {
-      // try again with a buffer that's large enough
-      n = size + 1;
-      delete [] buf;
-    }
-  }
-
-  setMessage(string(buf));
-
-
-#ifdef CVC4_DEBUG
-  LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
-  if(buffer != NULL){
-    if(buffer->getContents() == NULL) {
-      buffer->setContents(buf);
-    }
-  }
-#endif /* CVC4_DEBUG */
-  delete [] buf;
-}
-
-#ifdef CVC4_DEBUG
-
-/**
- * Special assertion failure handling in debug mode; in non-debug
- * builds, the exception is thrown from the macro.  We factor out this
- * additional logic so as not to bloat the code at every Assert()
- * expansion.
- *
- * Note this name is prefixed with "debug" because it is included in
- * debug builds only; in debug builds, it handles all assertion
- * failures (even those that exist in non-debug builds).
- */
-void debugAssertionFailed(const AssertionException& thisException,
-                          const char* propagatingException) {
-  static thread_local bool alreadyFired = false;
-
-  if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
-    throw thisException;
-  }
-
-  alreadyFired = true;
-
-  // propagatingException is the propagating exception, but can be
-  // NULL if the propagating exception is not a CVC4::Exception.
-  Warning() << "===========================================" << std::endl
-            << "An assertion failed during stack unwinding:" << std::endl;
-  if(propagatingException != NULL) {
-    Warning() << "The propagating exception is:" << std::endl
-              << propagatingException << std::endl
-              << "===========================================" << std::endl;
-    Warning() << "The newly-thrown exception is:" << std::endl;
-  } else {
-    Warning() << "The propagating exception is unknown." << std::endl;
-  }
-  Warning() << thisException << std::endl
-            << "===========================================" << std::endl;
-
-  terminate();
-}
-
-#endif /* CVC4_DEBUG */
-
-}/* CVC4 namespace */