* Add virtual destructors to CnfStream, Theory, OutputChannel, and

  ExplainOutputChannel.  Safer and stops a compiler warning.

* node attributes: fix compiler warnings on 64-bit.

* Node: add asserts to make sure the current NodeManager is non-NULL
  when it's needed.  This can happen when public-facing functions
  don't properly set the node manager, and it can look like a bug in
  another part of the library.  Also some code format cleanup.

* configure.ac, config/cvc4.m4: added --enable-static-binary (see
  discussion on bug 32), fixed bad configure lines (bug 19), added
  documentation for some things.

* config.h.in: removed; it's auto-generated.

9 files changed, 159 insertions, 164 deletions

diff --git a/config.h.in b/config.h.in
deleted file mode 100644
index 798fd63fa..000000000
--- a/config.h.in
+++ /dev/null
@@ -1,111 +0,0 @@
-/* config.h.in.  Generated from configure.ac by autoheader.  */
-
-/* Major component of the version of CVC4. */
-#undef CVC4_MAJOR
-
-/* Minor component of the version of CVC4. */
-#undef CVC4_MINOR
-
-/* Release component of the version of CVC4. */
-#undef CVC4_RELEASE
-
-/* Full release string for CVC4. */
-#undef CVC4_RELEASE_STRING
-
-/* Define to 1 if you have the <dlfcn.h> header file. */
-#undef HAVE_DLFCN_H
-
-/* Define to 1 if you have the <getopt.h> header file. */
-#undef HAVE_GETOPT_H
-
-/* Define to 1 if you have the <inttypes.h> header file. */
-#undef HAVE_INTTYPES_H
-
-/* Define to 1 if you have the `gmp' library (-lgmp). */
-#undef HAVE_LIBGMP
-
-/* Define to 1 if you have the <memory.h> header file. */
-#undef HAVE_MEMORY_H
-
-/* Define to 1 if stdbool.h conforms to C99. */
-#undef HAVE_STDBOOL_H
-
-/* Define to 1 if you have the <stdint.h> header file. */
-#undef HAVE_STDINT_H
-
-/* Define to 1 if you have the <stdlib.h> header file. */
-#undef HAVE_STDLIB_H
-
-/* Define to 1 if you have the <strings.h> header file. */
-#undef HAVE_STRINGS_H
-
-/* Define to 1 if you have the <string.h> header file. */
-#undef HAVE_STRING_H
-
-/* Define to 1 if you have the <sys/stat.h> header file. */
-#undef HAVE_SYS_STAT_H
-
-/* Define to 1 if you have the <sys/types.h> header file. */
-#undef HAVE_SYS_TYPES_H
-
-/* Define to 1 if you have the <unistd.h> header file. */
-#undef HAVE_UNISTD_H
-
-/* Define to 1 if the system has the type `_Bool'. */
-#undef HAVE__BOOL
-
-/* Define to the sub-directory in which libtool stores uninstalled libraries.
-   */
-#undef LT_OBJDIR
-
-/* Name of package */
-#undef PACKAGE
-
-/* Define to the address where bug reports for this package should be sent. */
-#undef PACKAGE_BUGREPORT
-
-/* Define to the full name of this package. */
-#undef PACKAGE_NAME
-
-/* Define to the full name and version of this package. */
-#undef PACKAGE_STRING
-
-/* Define to the one symbol short name of this package. */
-#undef PACKAGE_TARNAME
-
-/* Define to the home page for this package. */
-#undef PACKAGE_URL
-
-/* Define to the version of this package. */
-#undef PACKAGE_VERSION
-
-/* Define to 1 if you have the ANSI C header files. */
-#undef STDC_HEADERS
-
-/* Version number of package */
-#undef VERSION
-
-/* Define for Solaris 2.5.1 so the uint32_t typedef from <sys/synch.h>,
-   <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
-   #define below would cause a syntax error. */
-#undef _UINT32_T
-
-/* Define for Solaris 2.5.1 so the uint64_t typedef from <sys/synch.h>,
-   <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
-   #define below would cause a syntax error. */
-#undef _UINT64_T
-
-/* Define to `unsigned int' if <sys/types.h> does not define. */
-#undef size_t
-
-/* Define to the type of an unsigned integer type of width exactly 16 bits if
-   such a type exists and the standard includes do not define it. */
-#undef uint16_t
-
-/* Define to the type of an unsigned integer type of width exactly 32 bits if
-   such a type exists and the standard includes do not define it. */
-#undef uint32_t
-
-/* Define to the type of an unsigned integer type of width exactly 64 bits if
-   such a type exists and the standard includes do not define it. */
-#undef uint64_t
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 42dfaead5..1cde462b5 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -18,7 +18,8 @@ for ac_option
 do
   case $ac_option in
     -*|*=*) ;;
-    *) ac_cvc4_build_profile_set=yes
+    production|debug|default|competition)
+       ac_cvc4_build_profile_set=yes
        AC_MSG_NOTICE([CVC4: building profile $ac_option])
        ac_option="--with-build=$ac_option" ;;
   esac
diff --git a/configure.ac b/configure.ac
index 36f6d6c16..8c1141b9d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -4,7 +4,7 @@
 dnl Preprocess CL args. Defined in config/cvc4.m4
 CVC4_AC_INIT
 
-AC_PREREQ(2.64)
+AC_PREREQ(2.61)
 AC_INIT
 AC_CONFIG_SRCDIR([src/include/cvc4_config.h])
 AC_CONFIG_AUX_DIR([config])
@@ -30,7 +30,7 @@ CVC4_RELEASE_STRING=prerelease
 #
 # For more information, see:
 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
-# For guidance on when to change the version number, refer to the 
+# For guidance on when to change the version number, refer to the
 # developer's guide.
 
 CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
@@ -195,10 +195,24 @@ case "$with_build" in
     ;;
 esac
 
+# permit a static binary
+AC_MSG_CHECKING([whether to build a static binary])
+AC_ARG_ENABLE([static-binary],
+     [AS_HELP_STRING([--enable-static-binary],
+                     [build a statically-linked binary [default=no]])])
+if test -z "${enable_static_binary+set}"; then
+  enable_static_binary=no
+fi
+AC_MSG_RESULT([$enable_static_binary])
+if test "${enable_static_binary}" = yes -a "${enable_static}" != yes; then
+  enable_static=yes
+  AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
+fi
+
 AC_MSG_CHECKING([whether to optimize libcvc4])
 
 AC_ARG_ENABLE([optimized],
-  [AS_HELP_STRING([--enable-optimized],       
+  [AS_HELP_STRING([--enable-optimized],
      [optimize the build])])
 
 if test -z "${enable_optimized+set}"; then
@@ -213,8 +227,8 @@ fi
 
 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 
-AC_ARG_ENABLE([debug-symbols],   
-  [AS_HELP_STRING([--disable-debug-symbols],  
+AC_ARG_ENABLE([debug-symbols],
+  [AS_HELP_STRING([--disable-debug-symbols],
      [do not include debug symbols in libcvc4])])
 
 if test -z "${enable_debug_symbols+set}"; then
@@ -229,8 +243,8 @@ fi
 
 AC_MSG_CHECKING([whether to include assertions in build])
 
-AC_ARG_ENABLE([assertions],      
-  [AS_HELP_STRING([--disable-assertions],     
+AC_ARG_ENABLE([assertions],
+  [AS_HELP_STRING([--disable-assertions],
      [turn off assertions in build])])
 
 if test -z "${enable_assertions+set}"; then
@@ -244,8 +258,8 @@ if test "$enable_assertions" = yes; then
 fi
 
 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
-AC_ARG_ENABLE([tracing],         
-  [AS_HELP_STRING([--disable-tracing],        
+AC_ARG_ENABLE([tracing],
+  [AS_HELP_STRING([--disable-tracing],
      [remove all tracing code from CVC4])])
 
 if test -z "${enable_tracing+set}"; then
@@ -259,8 +273,8 @@ if test "$enable_tracing" = yes; then
 fi
 
 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
-AC_ARG_ENABLE([muzzle],          
-  [AS_HELP_STRING([--enable-muzzle],          
+AC_ARG_ENABLE([muzzle],
+  [AS_HELP_STRING([--enable-muzzle],
      [completely silence CVC4; remove ALL non-result output from build])])
 
 if test -z "${enable_muzzle+set}"; then
@@ -274,8 +288,8 @@ if test "$enable_muzzle" = yes; then
 fi
 
 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
-AC_ARG_ENABLE([coverage],        
-  [AS_HELP_STRING([--enable-coverage],        
+AC_ARG_ENABLE([coverage],
+  [AS_HELP_STRING([--enable-coverage],
      [build with support for gcov coverage testing])])
 
 if test -z "${enable_coverage+set}"; then
@@ -291,8 +305,8 @@ fi
 
 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 
-AC_ARG_ENABLE([profiling],       
-  [AS_HELP_STRING([--enable-profiling],       
+AC_ARG_ENABLE([profiling],
+  [AS_HELP_STRING([--enable-profiling],
      [build with support for gprof profiling])])
 
 if test -z "${enable_profiling+set}"; then
@@ -325,9 +339,11 @@ DX_PS_FEATURE(OFF)
 DX_DOT_FEATURE(OFF)
 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
 
+AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
+
 AC_SUBST([CXXTEST])
 
-AC_ARG_WITH([cxxtest-dir], 
+AC_ARG_WITH([cxxtest-dir],
   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
   [CXXTEST="$withval"])
 
@@ -389,7 +405,7 @@ AC_LIB_ANTLR
 AC_CHECK_HEADERS([getopt.h unistd.h])
 
 # Checks for typedefs, structures, and compiler characteristics.
-AC_HEADER_STDBOOL
+#AC_HEADER_STDBOOL
 AC_TYPE_UINT16_T
 AC_TYPE_UINT32_T
 AC_TYPE_UINT64_T
@@ -407,7 +423,7 @@ if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
 if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
 AC_SUBST(BUILDING_SHARED)
 AC_SUBST(BUILDING_STATIC)
-AM_CONDITIONAL([STATIC_BINARY], [test "$enable_shared" != yes -a "$enable_static" = yes])
+AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
 
 AC_SUBST(CVC4_LIBRARY_VERSION)
 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
@@ -478,6 +494,10 @@ gcov support : $enable_coverage
 gprof support: $enable_profiling
 unit tests   : $support_unit_tests
 
+static libs  : $enable_static
+shared libs  : $enable_shared
+static binary: $enable_static_binary
+
 CPPFLAGS     : $CPPFLAGS
 CXXFLAGS     : $CXXFLAGS
 LDFLAGS      : $LDFLAGS
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 12de9eb5f..1d2705240 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -56,7 +56,7 @@ namespace expr {
 
 struct AttrHashFcn {
   enum { LARGE_PRIME = 1 };
-  std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
+  std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const {
     return p.first * LARGE_PRIME + p.second.hash();
   }
 };
@@ -122,7 +122,7 @@ struct KindTableMapping {
 
 // use a TAG to indicate which table it should be in
 template <class value_type>
-struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
+struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
 
 template <>
 class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
@@ -215,19 +215,23 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
 
 public:
 
-  typedef std::pair<unsigned, SoftNode> key_type;
+  typedef std::pair<uint64_t, SoftNode> key_type;
   typedef bool data_type;
   typedef std::pair<const key_type, data_type> value_type;
 
   typedef BitIterator iterator;
   typedef ConstBitIterator const_iterator;
 
-  BitIterator find(const std::pair<unsigned, SoftNode>& k) {
+  BitIterator find(const std::pair<uint64_t, SoftNode>& k) {
     super::iterator i = super::find(k.second);
     if(i == super::end()) {
       return BitIterator();
     }
-    Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
+    Debug.printf("boolattr",
+                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+                 &(*i).second,
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
     return BitIterator(*i, k.first);
   }
 
@@ -235,12 +239,16 @@ public:
     return BitIterator();
   }
 
-  ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const {
+  ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
     super::const_iterator i = super::find(k.second);
     if(i == super::end()) {
       return ConstBitIterator();
     }
-    Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
+    Debug.printf("boolattr",
+                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+                 &(*i).second,
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
     return ConstBitIterator(*i, k.first);
   }
 
@@ -248,7 +256,7 @@ public:
     return ConstBitIterator();
   }
 
-  BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
+  BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
     uint64_t& word = super::operator[](k.second);
     return BitAccessor(word, k.first);
   }
@@ -268,18 +276,18 @@ struct Attribute {
   /** cleanup routine when the Node goes away */
   static inline void cleanup(const value_t&) {}
 
-  static inline unsigned getId() { return s_id; }
-  static inline unsigned getHashValue() { return s_hashValue; }
+  static inline uint64_t getId() { return s_id; }
+  static inline uint64_t getHashValue() { return s_hashValue; }
 
   static const bool has_default_value = false;
 
 private:
 
   /** an id */
-  static const unsigned s_id;
+  static const uint64_t s_id;
 
   /** an extra hash value (to avoid same-value-type collisions) */
-  static const unsigned s_hashValue;
+  static const uint64_t s_hashValue;
 };
 
 /**
@@ -294,13 +302,13 @@ struct Attribute<T, bool> {
   /** cleanup routine when the Node goes away */
   static inline void cleanup(const bool&) {}
 
-  static inline unsigned getId() { return s_id; }
-  static inline unsigned getHashValue() { return s_hashValue; }
+  static inline uint64_t getId() { return s_id; }
+  static inline uint64_t getHashValue() { return s_hashValue; }
 
   static const bool has_default_value = true;
   static const bool default_value = false;
 
-  static inline unsigned checkID(unsigned id) {
+  static inline uint64_t checkID(uint64_t id) {
     AlwaysAssert(id <= 63,
                  "Too many boolean node attributes registered during initialization !");
     return id;
@@ -309,10 +317,10 @@ struct Attribute<T, bool> {
 private:
 
   /** a bit assignment */
-  static const unsigned s_id;
+  static const uint64_t s_id;
 
   /** an extra hash value (to avoid same-value-type collisions) */
-  static const unsigned s_hashValue;
+  static const uint64_t s_hashValue;
 };
 
 // SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
@@ -323,11 +331,11 @@ namespace attr {
 
   template <class T>
   struct LastAttributeId {
-    static unsigned s_id;
+    static uint64_t s_id;
   };
 
   template <class T>
-  unsigned LastAttributeId<T>::s_id = 0;
+  uint64_t LastAttributeId<T>::s_id = 0;
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarName, std::string> VarNameAttr;
@@ -336,16 +344,16 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 
 template <class T, class value_t>
-const unsigned Attribute<T, value_t>::s_id =
+const uint64_t Attribute<T, value_t>::s_id =
   attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
 template <class T, class value_t>
-const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
 
 template <class T>
-const unsigned Attribute<T, bool>::s_id =
+const uint64_t Attribute<T, bool>::s_id =
   Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
 template <class T>
-const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
 
 class AttributeManager;
 
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 644570b24..79490d58e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -97,51 +97,83 @@ Node& Node::operator=(const Node& e) {
 }
 
 Node Node::eqExpr(const Node& right) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
 }
 
 Node Node::notExpr() const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(NOT, *this);
 }
 
 Node Node::andExpr(const Node& right) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(AND, *this, right);
 }
 
 Node Node::orExpr(const Node& right) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(OR, *this, right);
 }
 
 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 }
 
 Node Node::iffExpr(const Node& right) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(IFF, *this, right);
 }
 
 Node Node::impExpr(const Node& right) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 }
 
 Node Node::xorExpr(const Node& right) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 }
 
-static void indent(ostream & o, int indent){
-  for(int i=0; i < indent; i++)
+static void indent(ostream & o, int indent) {
+  for(int i=0; i < indent; i++) {
     o << ' ';
+  }
 }
 
 void Node::printAst(ostream & o, int ind) const {
   indent(o, ind);
   o << '(';
   o << getKind();
-  if(getKind() == VARIABLE){
+  if(getKind() == VARIABLE) {
     o << ' ' << getId();
-
-  }else if(getNumChildren() >= 1){
-    for(Node::iterator child = begin(); child != end(); ++child){
+  } else if(getNumChildren() >= 1) {
+    for(Node::iterator child = begin(); child != end(); ++child) {
       o << endl;
       (*child).printAst(o, ind + 1);
     }
diff --git a/src/expr/node.h b/src/expr/node.h
index 463ff8144..a39dc5b7e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -48,7 +48,6 @@ using CVC4::expr::NodeValue;
 class Node {
 
   friend class NodeValue;
-  friend class SoftNode;
 
   /** A convenient null-valued encapsulated pointer */
   static Node s_null;
@@ -106,7 +105,7 @@ public:
   bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
 
   Node operator[](int i) const {
-    Assert(i >= 0 && i < d_ev->d_nchildren);
+    Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
     return Node(d_ev->d_children[i]);
   }
 
@@ -130,9 +129,11 @@ public:
   Node impExpr(const Node& right) const;
   Node xorExpr(const Node& right) const;
 
+  /*
   Node plusExpr(const Node& right) const;
   Node uMinusExpr() const;
   Node multExpr(const Node& right) const;
+  */
 
   inline Kind getKind() const;
 
@@ -171,9 +172,9 @@ public:
    * @param indent number of spaces to indent the formula by.
    */
   void printAst(std::ostream & o, int indent = 0) const;
-  
+
 private:
-  
+
   /**
    * Pretty printer for use within gdb
    * This is not intended to be used outside of gdb.
@@ -262,18 +263,30 @@ inline size_t Node::getNumChildren() const {
 
 template <class AttrKind>
 inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
 }
 
 template <class AttrKind>
 inline bool Node::hasAttribute(const AttrKind&,
                                typename AttrKind::value_type* ret) {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
 }
 
 template <class AttrKind>
 inline void Node::setAttribute(const AttrKind&,
                                const typename AttrKind::value_type& value) {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 1bb71860c..d7bb3c265 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -116,6 +116,14 @@ public:
   CnfStream(SatSolver* satSolver);
 
   /**
+   * Destructs a CnfStream.  This implementation does nothing, but we
+   * need a virtual destructor for safety in case subclasses have a
+   * destructor.
+   */
+  virtual ~CnfStream() {
+  }
+
+  /**
    * Converts and asserts a formula.
    * @param node node to convert and assert
    * @param whether the sat solver can choose to remove this clause
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index cec499a13..c530434f5 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -28,6 +28,14 @@ class OutputChannel {
 public:
 
   /**
+   * Destructs an OutputChannel.  This implementation does nothing,
+   * but we need a virtual destructor for safety in case subclasses
+   * have a destructor.
+   */
+  virtual ~OutputChannel() {
+  }
+
+  /**
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
@@ -68,6 +76,14 @@ class ExplainOutputChannel {
 public:
 
   /**
+   * Destructs an ExplainOutputChannel.  This implementation does
+   * nothing, but we need a virtual destructor for safety in case
+   * subclasses have a destructor.
+   */
+  virtual ~ExplainOutputChannel() {
+  }
+
+  /**
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.  The default implementation never
    * interrupts.
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 8b83f71cf..dffc99053 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -58,12 +58,20 @@ public:
   static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
 
   /**
-   * Construct a theory.
+   * Construct a Theory.
    */
   Theory() {
   }
 
   /**
+   * Destructs a Theory.  This implementation does nothing, but we
+   * need a virtual destructor for safety in case subclasses have a
+   * destructor.
+   */
+  virtual ~Theory() {
+  }
+
+  /**
    * Prepare for a Node.
    *
    * When get() is called to get the next thing off the theory queue,