1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 23cf5f5d0..74fc16764 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -48,7 +48,6 @@ public:
 public:
   std::vector< Node > d_nodes;
 public:
-  void debugPrint( const char* c );
   IMGenerator* getGenerator() { return d_mg; }
 public:
   /** reset instantiation round (call this whenever equivalence classes have changed) */
@@ -123,6 +122,14 @@ public:
     out << " )";
     */
   }
+  void debugPrint( const char * c ) {
+    Trace(c) << "TRIGGER( ";
+    for( int i=0; i<(int)d_nodes.size(); i++ ){
+      if( i>0 ){ Trace(c) << ", "; }
+      Trace(c) << d_nodes[i];
+    }
+    Trace(c) << " )";
+  }
 };
 
 inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {