2 files changed, 12 insertions, 22 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 9b5ac66d3..a016c7897 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -60,24 +60,19 @@ Node buildConjunct(const std::vector<TNode> &assumptions) {
 }  // namespace helper
 
 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context* c,
-                   context::UserContext* u,
-                   OutputChannel& out,
-                   Valuation valuation,
-                   const LogicInfo& logicInfo,
-                   ProofNodeManager* pnm)
-    : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
+TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_FP, env, out, valuation),
       d_notification(*this),
-      d_registeredTerms(u),
-      d_conv(new FpConverter(u)),
+      d_registeredTerms(getUserContext()),
+      d_conv(new FpConverter(getUserContext())),
       d_expansionRequested(false),
-      d_realToFloatMap(u),
-      d_floatToRealMap(u),
-      d_abstractionMap(u),
-      d_rewriter(u),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::fp::", false),
-      d_wbFactsCache(u)
+      d_realToFloatMap(getUserContext()),
+      d_floatToRealMap(getUserContext()),
+      d_abstractionMap(getUserContext()),
+      d_rewriter(getUserContext()),
+      d_state(getSatContext(), getUserContext(), valuation),
+      d_im(*this, d_state, d_pnm, "theory::fp::", false),
+      d_wbFactsCache(getUserContext())
 {
   // indicate we are using the default theory state and inference manager
   d_theoryState = &d_state;
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 14779cc3d..1e1041980 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -39,12 +39,7 @@ class TheoryFp : public Theory
 {
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-  TheoryFp(context::Context* c,
-           context::UserContext* u,
-           OutputChannel& out,
-           Valuation valuation,
-           const LogicInfo& logicInfo,
-           ProofNodeManager* pnm = nullptr);
+  TheoryFp(Env& env, OutputChannel& out, Valuation valuation);
 
   //--------------------------------- initialization
   /** Get the official theory rewriter of this theory. */