1 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index a86984cca..8ddf809b6 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -27,6 +27,8 @@
 namespace CVC4 {
 namespace theory {
 
+class Theory;
+
 /**
  * A LemmaStatus, returned from OutputChannel::lemma(), provides information
  * about the lemma added.  In particular, it contains the T-rewritten lemma
@@ -206,8 +208,14 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource() throw() {
-  }
+  virtual void spendResource() throw() {}
+
+  /** Handle user attribute
+    *   Associates theory t with the attribute attr.  Theory t will be
+    *   notifed whenever an attribute of name attr is set on a node.
+    *   This can happen through, for example, the SMT LIB v2 language.
+    */
+  virtual void handleUserAttribute( const char* attr, Theory* t ){}
 
 };/* class OutputChannel */