Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address. Resolves bug #263.

Also, some debugging improvements.

6 files changed, 63 insertions, 32 deletions

diff --git a/src/context/context.h b/src/context/context.h
index aabe4e7c2..6375707b9 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -577,7 +577,7 @@ public:
    * ContextMemoryManager as an argument.
    */
   void deleteSelf() {
-    Debug("context") << "deleteSelf(" << this << ")" << std::endl;
+    Debug("context") << "deleteSelf(" << this << ") " << typeid(*this).name() << std::endl;
     this->~ContextObj();
     ::operator delete(this);
   }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index cc7e89bc8..95f7c0437 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -900,8 +900,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
     nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
     nv->d_rc = 0;
     setUsed();
-    Debug("gc") << "creating node value " << nv
-                << " [" << nv->d_id << "]: " << *nv << "\n";
+    if(Debug.isOn("gc")) {
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: ";
+      nv->printAst(Debug("gc"));
+      Debug("gc") << std::endl;
+    }
     return nv;
   }
 
@@ -982,8 +986,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
 
       //poolNv = nv;
       d_nm->poolInsert(nv);
-      Debug("gc") << "creating node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv << "\n";
+      if(Debug.isOn("gc")) {
+        Debug("gc") << "creating node value " << nv
+                    << " [" << nv->d_id << "]: ";
+        nv->printAst(Debug("gc"));
+        Debug("gc") << std::endl;
+      }
       return nv;
     }
   } else {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4cde0c624..95124d297 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -202,8 +202,12 @@ void NodeManager::reclaimZombies() {
 
     // collect ONLY IF still zero
     if(nv->d_rc == 0) {
-      Debug("gc") << "deleting node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv << "\n";
+      if(Debug.isOn("gc")) {
+        Debug("gc") << "deleting node value " << nv
+                    << " [" << nv->d_id << "]: ";
+        nv->printAst(Debug("gc"));
+        Debug("gc") << std::endl;
+      }
 
       // remove from the pool
       kind::MetaKind mk = nv->getMetaKind();
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 9974df6ca..54266db13 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -185,10 +185,13 @@ class NodeManager {
 
     // if d_reclaiming is set, make sure we don't call
     // reclaimZombies(), because it's already running.
-    Debug("gc") << "zombifying node value " << nv
-                << " [" << nv->d_id << "]: " << *nv
-                << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
-                << std::endl;
+    if(Debug.isOn("gc")) {
+      Debug("gc") << "zombifying node value " << nv
+                  << " [" << nv->d_id << "]: ";
+      nv->printAst(Debug("gc"));
+      Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
+                  << std::endl;
+    }
     d_zombies.insert(nv);// FIXME multithreading
 
     if(!d_inReclaimZombies) {// FIXME multithreading
@@ -1269,8 +1272,12 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
   new (&nv->d_children) T(val);
 
   poolInsert(nv);
-  Debug("gc") << "creating node value " << nv
-              << " [" << nv->d_id << "]: " << *nv << "\n";
+  if(Debug.isOn("gc")) {
+    Debug("gc") << "creating node value " << nv
+                << " [" << nv->d_id << "]: ";
+    nv->printAst(Debug("gc"));
+    Debug("gc") << std::endl;
+  }
 
   return NodeClass(nv);
 }
diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h
index b11ebf957..418172235 100644
--- a/src/util/backtrackable.h
+++ b/src/util/backtrackable.h
@@ -1,3 +1,4 @@
+/*********************                                                        */
 /*! \file backtrackable.h
  ** \verbatim
  ** Original author: lianah
@@ -12,26 +13,26 @@
  **
  ** \brief Contains a backtrackable list
  **
- **
+ ** Contains a backtrackable list.
  **/
 
 #include "cvc4_private.h"
+
 #ifndef __CVC4__UTIL__BACKTRACKABLE_H
 #define __CVC4__UTIL__BACKTRACKABLE_H
 
-
 #include <cstdlib>
 #include <vector>
 #include "context/cdo.h"
 
-namespace CVC4{
+namespace CVC4 {
 
 template <class T> class List;
 template <class T> class List_iterator;
 template <class T> class Backtracker;
 
 template <class T>
-class ListNode{
+class ListNode {
 private:
   T data;
   ListNode<T>* next;
@@ -45,10 +46,10 @@ private:
 
   friend class List<T>;
   friend class List_iterator<T>;
-}; /*class ListNode */
+};/* class ListNode<T> */
 
 template <class T>
-class List_iterator: public std::iterator <std::forward_iterator_tag, T> {
+class List_iterator : public std::iterator <std::forward_iterator_tag, T> {
   friend class List<T>;
 
 public:
@@ -56,17 +57,20 @@ public:
   List_iterator<T>& operator++();
   List_iterator<T> operator++(int);
   bool operator!=(const List_iterator<T> & other) const;
+
 private:
   const ListNode<T>* pointee;
   List_iterator(const ListNode<T>* p) : pointee(p) {}
 
-}; /* class List_iterator */
+};/* class List_iterator<T> */
 
-template <class T> const T& List_iterator<T>::operator*() {
+template <class T>
+const T& List_iterator<T>::operator*() {
   return pointee->data;
 }
 
-template <class T> List_iterator<T>& List_iterator<T>::operator++() {
+template <class T>
+List_iterator<T>& List_iterator<T>::operator++() {
   Assert(pointee != NULL);
   pointee = pointee->next;
   while(pointee != NULL && pointee->empty ) {
@@ -75,19 +79,22 @@ template <class T> List_iterator<T>& List_iterator<T>::operator++() {
   return *this;
 }
 
-template <class T> List_iterator<T> List_iterator<T>::operator++(int) {
+template <class T>
+List_iterator<T> List_iterator<T>::operator++(int) {
   List_iterator<T> it = *this;
   ++*this;
   return it;
 }
 
-template <class T> bool List_iterator<T>::operator!=(const List_iterator<T>& other) const {
+template <class T>
+bool List_iterator<T>::operator!=(const List_iterator<T>& other) const {
   return (this->pointee != other.pointee);
 }
 
 // !! for the backtracking to work the lists must be allocated on the heap
 // therefore the hashmap from TNode to List<TNode> should store pointers!
-template <class T> class List {
+template <class T>
+class List {
   ListNode<T>* head;
   ListNode<T>* tail;
   ListNode<T>* ptr_to_head;
@@ -96,7 +103,7 @@ template <class T> class List {
   List (const List&) {}
 public:
   List(Backtracker<T>* b) : ptr_to_head(NULL), uninitialized(true), bck(b) {
-    head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>*));
+    head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>));
     head->next = NULL;
     head->empty = true;
   }
@@ -128,7 +135,7 @@ public:
   }
   void concat(List<T>* other);
   void unconcat(List<T>* other);
-}; /* class List */
+};/* class List */
 
 template <class T>
 void List<T>::append (const T& d) {
@@ -174,7 +181,8 @@ void List<T>::unconcat(List<T>* other) {
 
 /* Backtrackable Table */
 
-template <class T> class Backtracker {
+template <class T>
+class Backtracker {
   friend class List<T>;
   std::vector<std::pair<List<T>*,List<T>*> > undo_stack;
 
@@ -187,7 +195,7 @@ public:
   Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {}
   ~Backtracker() {}
 
-}; /*class Backtrackable */
+};/* class Backtrackable */
 
 template <class T>  void Backtracker<T>::notifyConcat(List<T>* a, List<T>* b) {
   curr_level++;
@@ -210,5 +218,7 @@ template <class T> void Backtracker<T>::checkConsistency() {
   }
   Assert(curr_level == pop_level);
 }
-} /* CVC4 namespace */
+
+}/* CVC4 namespace */
+
 #endif /* __CVC4__UTIL__BACKTRACKABLE_H */
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 428f051e0..70d486ff6 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -32,7 +32,8 @@ StatisticsRegistry* StatisticsRegistry::current() {
 void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
-  AlwaysAssert(registeredStats.find(s) == registeredStats.end());
+  AlwaysAssert(registeredStats.find(s) == registeredStats.end(),
+               "Statistic `%s' was already registered with this registry.", s->getName().c_str());
   registeredStats.insert(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat() */
@@ -40,7 +41,8 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
 void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
-  AlwaysAssert(registeredStats.find(s) != registeredStats.end());
+  AlwaysAssert(registeredStats.find(s) != registeredStats.end(),
+               "Statistic `%s' was not registered with this registry.", s->getName().c_str());
   registeredStats.erase(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat() */