2 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7bca9da74..c8ae3d844 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -56,7 +56,8 @@ TheoryUF::TheoryUF(context::Context* c,
       d_ho(nullptr),
       d_conflict(c, false),
       d_functionsTerms(c),
-      d_symb(u, instanceName)
+      d_symb(u, instanceName),
+      d_state(c, u, valuation)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
 
@@ -65,6 +66,8 @@ TheoryUF::TheoryUF(context::Context* c,
   {
     d_ufProofChecker.registerTo(pc);
   }
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheoryUF::~TheoryUF() {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 414a2dd6a..4d0a3126f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -219,6 +219,8 @@ private:
   TheoryUfRewriter d_rewriter;
   /** Proof rule checker */
   UfProofRuleChecker d_ufProofChecker;
+  /** A (default) theory state object */
+  TheoryState d_state;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */