1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 7d7da35c5..b25bf503d 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -99,6 +99,18 @@ public:
     throw(Interrupted, AssertionException) = 0;
 
   /**
+   * Request a split on a new theory atom.  This is equivalent to
+   * calling lemma({OR n (NOT n)}).
+   *
+   * @param n - a theory atom; must be of Boolean type
+   * @param safe - whether it is safe to be interrupted
+   */
+  void split(TNode n, bool safe = false)
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) {
+    lemma(n.orNode(n.notNode()));
+  }
+
+  /**
    * Provide an explanation in response to an explanation request.
    *
    * @param n - an explanation