2 files changed, 41 insertions, 37 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index dfd3c4803..b68687d54 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -55,42 +55,44 @@ Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, No
 }
 
 
-TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-  RMAXINT(LONG_MAX),
-  d_notify( *this ),
-  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
-  d_conflict(c, false),
-  d_infer(c),
-  d_infer_exp(c),
-  d_nf_pairs(c),
-  d_loop_antec(u),
-  d_length_intro_vars(u),
-  d_pregistered_terms_cache(u),
-  d_registered_terms_cache(u),
-  d_preproc(u),
-  d_preproc_cache(u),
-  d_extf_infer_cache(c),
-  d_congruent(c),
-  d_proxy_var(u),
-  d_proxy_var_to_length(u),
-  d_neg_ctn_eqlen(c),
-  d_neg_ctn_ulen(c),
-  d_neg_ctn_cached(u),
-  d_ext_func_terms(c),
-  d_regexp_memberships(c),
-  d_regexp_ucached(u),
-  d_regexp_ccached(c),
-  d_pos_memberships(c),
-  d_neg_memberships(c),
-  d_inter_cache(c),
-  d_inter_index(c),
-  d_processed_memberships(c),
-  d_regexp_ant(c),
-  d_input_vars(u),
-  d_input_var_lsum(u),
-  d_cardinality_lits(u),
-  d_curr_cardinality(c, 0)
+TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
+                             OutputChannel& out, Valuation valuation,
+                             const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, globals),
+      RMAXINT(LONG_MAX),
+      d_notify( *this ),
+      d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
+      d_conflict(c, false),
+      d_infer(c),
+      d_infer_exp(c),
+      d_nf_pairs(c),
+      d_loop_antec(u),
+      d_length_intro_vars(u),
+      d_pregistered_terms_cache(u),
+      d_registered_terms_cache(u),
+      d_preproc(u),
+      d_preproc_cache(u),
+      d_extf_infer_cache(c),
+      d_congruent(c),
+      d_proxy_var(u),
+      d_proxy_var_to_length(u),
+      d_neg_ctn_eqlen(c),
+      d_neg_ctn_ulen(c),
+      d_neg_ctn_cached(u),
+      d_ext_func_terms(c),
+      d_regexp_memberships(c),
+      d_regexp_ucached(u),
+      d_regexp_ccached(c),
+      d_pos_memberships(c),
+      d_neg_memberships(c),
+      d_inter_cache(c),
+      d_inter_index(c),
+      d_processed_memberships(c),
+      d_regexp_ant(c),
+      d_input_vars(u),
+      d_input_var_lsum(u),
+      d_cardinality_lits(u),
+      d_curr_cardinality(c, 0)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 40358649b..ddb800ee1 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -52,7 +52,9 @@ class TheoryStrings : public Theory {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
 public:
-  TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryStrings(context::Context* c, context::UserContext* u,
+                OutputChannel& out, Valuation valuation,
+                const LogicInfo& logicInfo, SmtGlobals* globals);
   ~TheoryStrings();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);