3 files changed, 32 insertions, 13 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 28404005c..280c55254 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -423,9 +423,9 @@ TypeNode NodeManager::computeType(TNode n, bool check)
   }
 
   setAttribute(n, TypeAttr(), typeNode);
-  setAttribute(n, TypeCheckedAttr(), 
+  setAttribute(n, TypeCheckedAttr(),
                check || getAttribute(n, TypeCheckedAttr()));
-  
+
   return typeNode;
 }
 
@@ -449,8 +449,10 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
       bool readyToCompute = true;
 
-      for( TNode::iterator it = m.begin(), end = m.end() ; it != end; ++it ) {
-        if( !hasAttribute(*it, TypeAttr()) 
+      for( TNode::iterator it = m.begin(), end = m.end();
+           it != end;
+           ++it ) {
+        if( !hasAttribute(*it, TypeAttr())
             || (check && !getAttribute(*it, TypeCheckedAttr())) ) {
           readyToCompute = false;
           worklist.push(*it);
@@ -459,23 +461,23 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
       if( readyToCompute ) {
         /* All the children have types, time to compute */
-        typeNode = computeType(m,check);
+        typeNode = computeType(m, check);
         worklist.pop();
-      } 
+      }
     } // end while
 
     /* Last type computed in loop should be the type of n */
-    Assert( typeNode == getAttribute(n,TypeAttr()) );
+    Assert( typeNode == getAttribute(n, TypeAttr()) );
   } else if( !hasType || needsCheck ) {
     /* We can compute the type top-down, without worrying about
        deep recursion. */
-    typeNode = computeType(n,check);
+    typeNode = computeType(n, check);
   }
 
   /* The type should be have been computed and stored. */
   Assert( hasAttribute(n, TypeAttr()) );
   /* The check should have happened, if we asked for it. */
-  Assert( !check || hasAttribute(n, TypeCheckedAttr()) );
+  Assert( !check || getAttribute(n, TypeCheckedAttr()) );
 
   Debug("getType") << "type of " << n << " is " << typeNode << std::endl;
   return typeNode;
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index f2dbd3bce..2ac1facb0 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -49,15 +49,32 @@
 // copy constructors.  The advantage is that with CVC4_UNDEFINED,
 // if something _does_ try to call the function, you get an error
 // at the point of the call (rather than a link error later).
+
+// CVC4_UNUSED is to mark something (e.g. local variable, function)
+// as being _possibly_ unused, so that the compiler generates no
+// warning about it.  This might be the case for e.g. a variable
+// only used in DEBUG builds.
+
 #ifdef __GNUC__
-#  define CVC4_UNDEFINED __attribute__((error("this function intentionally undefined")))
+#  if __GNUC__ > 4 || ( __GNUC__ == 4 && __GNUC_MINOR__ >= 3 )
+     /* error function attribute only exists in GCC >= 4.3.0 */
+#    define CVC4_UNDEFINED __attribute__((error("this function intentionally undefined")))
+#  else /* GCC < 4.3.0 */
+#    define CVC4_UNDEFINED
+#  endif /* GCC >= 4.3.0 */
 #else /* ! __GNUC__ */
 #  define CVC4_UNDEFINED
 #endif /* __GNUC__ */
 
+#ifdef __GNUC__
+#  define CVC4_UNUSED __attribute__((unused))
+#else /* ! __GNUC__ */
+#  define CVC4_UNUSED
+#endif /* __GNUC__ */
+
 #define EXPECT_TRUE(x) __builtin_expect( (x), true )
 #define EXPECT_FALSE(x) __builtin_expect( (x), false )
-#define NORETURN __attribute__ ((noreturn))
+#define CVC4_NORETURN __attribute__ ((noreturn))
 
 #ifndef NULL
 #  define NULL ((void*) 0)
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 38c75f0d3..fcd322e99 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -133,7 +133,7 @@ int runCvc4(int argc, char* argv[]) {
   cvc4_init();
 
   progPath = argv[0];
-  
+
   // Parse the options
   int firstArgIndex = options.parseOptions(argc, argv);
 
@@ -148,7 +148,7 @@ int runCvc4(int argc, char* argv[]) {
   } else if( options.version ) {
     *options.out << Configuration::about().c_str() << flush;
     exit(0);
-  } 
+  }
 
   segvNoSpin = options.segvNoSpin;