1 files changed, 14 insertions, 12 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5bb71532c..93df4fe38 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -37,22 +37,24 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 
-TheoryEngine::TheoryEngine(context::Context* ctxt)
+TheoryEngine::TheoryEngine(context::Context* context,
+                           context::UserContext* userContext)
 : d_propEngine(NULL),
-  d_context(ctxt),
+  d_context(context),
+  d_userContext(userContext),
   d_activeTheories(0),
-  d_sharedTerms(ctxt),
+  d_sharedTerms(context),
   d_atomPreprocessingCache(),
   d_possiblePropagations(),
-  d_hasPropagated(ctxt),
-  d_inConflict(ctxt, false),
+  d_hasPropagated(context),
+  d_inConflict(context, false),
   d_hasShutDown(false),
-  d_incomplete(ctxt, false),
-  d_sharedAssertions(ctxt),
+  d_incomplete(context, false),
+  d_sharedAssertions(context),
   d_logic(""),
-  d_propagatedLiterals(ctxt),
-  d_propagatedLiteralsIndex(ctxt, 0),
-  d_preRegistrationVisitor(this, ctxt),
+  d_propagatedLiterals(context),
+  d_propagatedLiteralsIndex(context, 0),
+  d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms)
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
@@ -378,10 +380,10 @@ void TheoryEngine::shutdown() {
   theory::Rewriter::shutdown();
 }
 
-theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
+theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
-  Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut);
+  Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitutionOut);
   Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
   return solveStatus;
 }