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.

3 files changed, 31 insertions, 12 deletions

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);
 }