1 files changed, 14 insertions, 11 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 261db8c87..acc242ab6 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -26,11 +26,12 @@
 #include <iosfwd>
 
 #include "context/cdqueue.h"
+#include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
-#include "smt/smt_globals.h"
-#include "smt_util/lemma_output_channel.h"
+#include "smt_util/lemma_channels.h"
 #include "smt_util/lemma_input_channel.h"
+#include "smt_util/lemma_output_channel.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
@@ -54,7 +55,9 @@ public:
               DecisionEngine* decisionEngine,
               context::Context* context,
               CnfStream* cnfStream,
-              SmtGlobals* globals);
+              std::ostream* replayLog,
+              ExprStream* replayStream,
+              LemmaChannels* globals);
 
   ~TheoryProxy();
 
@@ -110,11 +113,14 @@ public:
   TheoryEngine* d_theoryEngine;
 
 
-  /**
-   * Container for inputChannel, outputChannel, replayLog, and
-   * replayStream.
-   */
-  SmtGlobals* d_globals;
+  /** Container for inputChannel() and outputChannel(). */
+  LemmaChannels* d_channels;
+
+  /** Stream on which to log replay events. */
+  std::ostream* d_replayLog;
+
+  /** Stream for replaying decisions. */
+  ExprStream* d_replayStream;
 
   /** The lemma input channel we are using. */
   LemmaInputChannel* inputChannel();
@@ -122,9 +128,6 @@ public:
   /** The lemma output channel we are using. */
   LemmaOutputChannel* outputChannel();
 
-  std::ostream* replayLog();
-  ExprStream* replayStream();
-
   /** Queue of asserted facts */
   context::CDQueue<TNode> d_queue;