Merge branch 'master' into stdAttrsstdAttrs

1 files changed, 6 insertions, 4 deletions

diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index ca1a2fa6f..31017dea6 100644
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -28,14 +28,16 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-BranchAndBound::BranchAndBound(ArithState& s,
+BranchAndBound::BranchAndBound(Env& env,
+                               ArithState& s,
                                InferenceManager& im,
                                PreprocessRewriteEq& ppre,
                                ProofNodeManager* pnm)
-    : d_astate(s),
+    : EnvObj(env),
+      d_astate(s),
       d_im(im),
       d_ppre(ppre),
-      d_pfGen(new EagerProofGenerator(pnm, s.getUserContext())),
+      d_pfGen(new EagerProofGenerator(pnm, userContext())),
       d_pnm(pnm)
 {
 }
@@ -45,7 +47,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
   TrustNode lem = TrustNode::null();
   NodeManager* nm = NodeManager::currentNM();
   Integer floor = value.floor();
-  if (d_astate.options().arith.brabTest)
+  if (options().arith.brabTest)
   {
     Trace("integers") << "branch-round-and-bound enabled" << std::endl;
     Integer ceil = value.ceiling();