Lemmas on demand work, push-pop, some cleanup.

1 files changed, 0 insertions, 11 deletions

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 1c48c0160..269f28732 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -100,17 +100,6 @@ public:
     throw(Interrupted, AssertionException) = 0;
 
   /**
-   * Tell the core to add the following valid lemma as if it were a
-   * user assertion.  This should NOT be called during solving, only
-   * preprocessing.
-   *
-   * @param n - a theory lemma valid to be asserted
-   * @param safe - whether it is safe to be interrupted
-   */
-  virtual void augmentingLemma(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) = 0;
-
-  /**
    * Provide an explanation in response to an explanation request.
    *
    * @param n - an explanation