2 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e9ff60137..b808f4cd5 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,8 +34,8 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
+    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 98f486145..f24c10fc0 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -46,10 +46,14 @@ private:
   int d_baseDecLevel;
 
   eq::EqualityEngine* d_masterEqualityEngine;
+
 private:
-  void computeCareGraph();  
+  void computeCareGraph();
+
 public:
-  TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryQuantifiers(context::Context* c, context::UserContext* u,
+                    OutputChannel& out, Valuation valuation,
+                    const LogicInfo& logicInfo, SmtGlobals* globals);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);