1 files changed, 14 insertions, 12 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 31bee316a..e21b7ef7d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -30,18 +30,20 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_UF, c, u, out, valuation, logicInfo),
-  d_notify(*this),
-  /* The strong theory solver can be notified by EqualityEngine::init(),
-   * so make sure it's initialized first. */
-  d_thss(NULL),
-  d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
-  d_conflict(c, false),
-  d_literalsToPropagate(c),
-  d_literalsToPropagateIndex(c, 0),
-  d_functionsTerms(c),
-  d_symb(u)
+TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
+                   OutputChannel& out, Valuation valuation,
+                   const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals),
+      d_notify(*this),
+      /* The strong theory solver can be notified by EqualityEngine::init(),
+       * so make sure it's initialized first. */
+      d_thss(NULL),
+      d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
+      d_conflict(c, false),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_functionsTerms(c),
+      d_symb(u)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);