2 files changed, 21 insertions, 11 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 1392f8fab..6a8b4771b 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -38,16 +38,21 @@ namespace CVC4 {
 namespace theory {
 namespace sep {
 
-TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
-  d_lemmas_produced_c(u),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sep::ee", true),
-  d_conflict(c, false),
-  d_reduce(u),
-  d_infer(c),
-  d_infer_exp(c),
-  d_spatial_assertions(c)
+TheorySep::TheorySep(Environment* env,
+                     context::Context* c,
+                     context::UserContext* u,
+                     OutputChannel& out,
+                     Valuation valuation,
+                     const LogicInfo& logicInfo)
+    : Theory(THEORY_SEP, env, c, u, out, valuation, logicInfo),
+      d_lemmas_produced_c(u),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::sep::ee", true),
+      d_conflict(c, false),
+      d_reduce(u),
+      d_infer(c),
+      d_infer_exp(c),
+      d_spatial_assertions(c)
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index ae044f6d7..dd3658fce 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -63,7 +63,12 @@ class TheorySep : public Theory {
                         bool pol, bool hasPol, bool underSpatial );
 
  public:
-  TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheorySep(Environment* env,
+            context::Context* c,
+            context::UserContext* u,
+            OutputChannel& out,
+            Valuation valuation,
+            const LogicInfo& logicInfo);
   ~TheorySep();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;