1 files changed, 10 insertions, 8 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 510e6d585..a3fd50d8c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -32,6 +32,7 @@
 #include <string>
 #include <unordered_set>
 
+#include "base/check.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
@@ -411,14 +412,16 @@ public:
 
   /** Subscribe to NodeManager events */
   void subscribeEvents(NodeManagerListener* listener) {
-    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
+    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener)
+           == d_listeners.end())
+        << "listener already subscribed";
     d_listeners.push_back(listener);
   }
 
   /** Unsubscribe from NodeManager events */
   void unsubscribeEvents(NodeManagerListener* listener) {
     std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
-    Assert(elt != d_listeners.end(), "listener not subscribed");
+    Assert(elt != d_listeners.end()) << "listener not subscribed";
     d_listeners.erase(elt);
   }
   
@@ -1177,14 +1180,14 @@ inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
 }
 
 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
-  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
-         "NodeValue already in the pool!");
+  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end())
+      << "NodeValue already in the pool!";
   d_nodeValuePool.insert(nv);// FIXME multithreading
 }
 
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
-  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
-         "NodeValue is not in the pool!");
+  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end())
+      << "NodeValue is not in the pool!";
 
   d_nodeValuePool.erase(nv);// FIXME multithreading
 }
@@ -1240,8 +1243,7 @@ inline bool NodeManager::hasOperator(Kind k) {
   case kind::metakind::CONSTANT:
     return false;
 
-  default:
-    Unhandled(mk);
+  default: Unhandled() << mk;
   }
 }