pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164)

1 files changed, 74 insertions, 71 deletions

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 8f6fa7b14..68758f766 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -48,6 +48,8 @@ class TestPPWhiteBVGauss : public TestSmt
     d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
         d_smtEngine.get(), d_smtEngine->getEnv(), nullptr));
 
+    d_bv_gauss.reset(new BVGauss(d_preprocContext.get()));
+
     d_zero = bv::utils::mkZero(16);
 
     d_p = bv::utils::mkConcat(
@@ -147,7 +149,7 @@ class TestPPWhiteBVGauss : public TestSmt
     std::cout << "Input: " << std::endl;
     print_matrix_dbg(rhs, lhs);
 
-    ret = BVGauss::gaussElim(prime, resrhs, reslhs);
+    ret = d_bv_gauss->gaussElim(prime, resrhs, reslhs);
 
     std::cout << "BVGauss::Result: "
               << (ret == BVGauss::Result::INVALID
@@ -199,6 +201,7 @@ class TestPPWhiteBVGauss : public TestSmt
   }
 
   std::unique_ptr<PreprocessingPassContext> d_preprocContext;
+  std::unique_ptr<BVGauss> d_bv_gauss;
 
   Node d_p;
   Node d_x;
@@ -262,7 +265,7 @@ TEST_F(TestPPWhiteBVGauss, elim_mod)
          {Integer(2), Integer(3), Integer(5)},
          {Integer(4), Integer(0), Integer(5)}};
   std::cout << "matrix 0, modulo 0" << std::endl;  // throws
-  ASSERT_DEATH(BVGauss::gaussElim(Integer(0), rhs, lhs), "prime > 0");
+  ASSERT_DEATH(d_bv_gauss->gaussElim(Integer(0), rhs, lhs), "prime > 0");
   std::cout << "matrix 0, modulo 1" << std::endl;
   testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE);
   std::cout << "matrix 0, modulo 2" << std::endl;
@@ -931,7 +934,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
   std::unordered_map<Node, Node> res;
-  BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
   ASSERT_EQ(res[d_x], d_three32);
@@ -1037,7 +1040,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
   std::unordered_map<Node, Node> res;
-  BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
   ASSERT_EQ(res[d_x], d_three32);
@@ -1075,7 +1078,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1199,7 +1202,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1321,7 +1324,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1419,7 +1422,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
       d_eight);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1562,7 +1565,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
       d_thirty);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1713,7 +1716,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
       d_thirty);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 1);
 
@@ -1820,7 +1823,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
       kind::EQUAL, d_nodeManager->mkNode(kind::BITVECTOR_UREM, w, d_p), d_two);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 3);
 
@@ -1915,7 +1918,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -2086,7 +2089,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -2224,7 +2227,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
       d_five);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
 
@@ -2285,7 +2288,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
       bv::utils::mkConcat(d_zero, d_nine));
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
 
@@ -2353,7 +2356,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid)
       bv::utils::mkConcat(d_zero, d_nine));
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::INVALID);
 }
 
@@ -2627,15 +2630,15 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw1)
 {
-  ASSERT_EQ(BVGauss::getMinBwExpr(bv::utils::mkConst(32, 11)), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(bv::utils::mkConst(32, 11)), 4);
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(d_p), 4);
-  ASSERT_EQ(BVGauss::getMinBwExpr(d_x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_x), 16);
 
   Node extp = bv::utils::mkExtract(d_p, 4, 0);
-  ASSERT_EQ(BVGauss::getMinBwExpr(extp), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(extp), 4);
   Node extx = bv::utils::mkExtract(d_x, 4, 0);
-  ASSERT_EQ(BVGauss::getMinBwExpr(extx), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(extx), 5);
 
   Node zextop8 =
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(8));
@@ -2647,132 +2650,132 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1)
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(40));
 
   Node zext40p = d_nodeManager->mkNode(zextop8, d_p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext40p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40p), 4);
   Node zext40x = d_nodeManager->mkNode(zextop8, d_x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext40x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40x), 16);
 
   Node zext48p = d_nodeManager->mkNode(zextop16, d_p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p), 4);
   Node zext48x = d_nodeManager->mkNode(zextop16, d_x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x), 16);
 
   Node p8 = d_nodeManager->mkConst<BitVector>(BitVector(8, 11u));
   Node x8 = d_nodeManager->mkVar("x8", d_nodeManager->mkBitVectorType(8));
 
   Node zext48p8 = d_nodeManager->mkNode(zextop40, p8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48p8), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p8), 4);
   Node zext48x8 = d_nodeManager->mkNode(zextop40, x8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48x8), 8);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x8), 8);
 
   Node mult1p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extp, extp);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult1p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1p), 5);
   Node mult1x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extx, extx);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult1x), 0);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1x), 0);
 
   Node mult2p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult2p), 7);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2p), 7);
   Node mult2x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult2x), 32);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2x), 32);
 
   NodeBuilder nbmult3p(kind::BITVECTOR_MULT);
   nbmult3p << zext48p << zext48p << zext48p;
   Node mult3p = nbmult3p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult3p), 11);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3p), 11);
   NodeBuilder nbmult3x(kind::BITVECTOR_MULT);
   nbmult3x << zext48x << zext48x << zext48x;
   Node mult3x = nbmult3x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult3x), 48);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3x), 48);
 
   NodeBuilder nbmult4p(kind::BITVECTOR_MULT);
   nbmult4p << zext48p << zext48p8 << zext48p;
   Node mult4p = nbmult4p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult4p), 11);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4p), 11);
   NodeBuilder nbmult4x(kind::BITVECTOR_MULT);
   nbmult4x << zext48x << zext48x8 << zext48x;
   Node mult4x = nbmult4x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult4x), 40);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4x), 40);
 
   Node concat1p = bv::utils::mkConcat(d_p, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat1p), 52);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1p), 52);
   Node concat1x = bv::utils::mkConcat(d_x, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat1x), 64);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1x), 64);
 
   Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat2p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2p), 4);
   Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat2x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2x), 16);
 
   Node udiv1p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv1p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1p), 1);
   Node udiv1x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv1x), 48);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1x), 48);
 
   Node udiv2p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv2p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2p), 1);
   Node udiv2x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv2x), 48);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2x), 48);
 
   Node urem1p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem1p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1p), 1);
   Node urem1x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem1x), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1x), 1);
 
   Node urem2p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem2p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2p), 1);
   Node urem2x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem2x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2x), 16);
 
   Node urem3p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p8, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem3p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3p), 1);
   Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3x), 8);
 
   Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extp, extp);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add1p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1p), 5);
   Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extx, extx);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add1x), 0);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1x), 0);
 
   Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40p, zext40p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add2p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2p), 5);
   Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40x, zext40x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add2x), 17);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2x), 17);
 
   Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48p8, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add3p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3p), 5);
   Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48x8, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3x), 17);
 
   NodeBuilder nbadd4p(kind::BITVECTOR_ADD);
   nbadd4p << zext48p << zext48p << zext48p;
   Node add4p = nbadd4p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4p), 6);
   NodeBuilder nbadd4x(kind::BITVECTOR_ADD);
   nbadd4x << zext48x << zext48x << zext48x;
   Node add4x = nbadd4x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4x), 18);
 
   NodeBuilder nbadd5p(kind::BITVECTOR_ADD);
   nbadd5p << zext48p << zext48p8 << zext48p;
   Node add5p = nbadd5p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5p), 6);
   NodeBuilder nbadd5x(kind::BITVECTOR_ADD);
   nbadd5x << zext48x << zext48x8 << zext48x;
   Node add5x = nbadd5x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5x), 18);
 
   NodeBuilder nbadd6p(kind::BITVECTOR_ADD);
   nbadd6p << zext48p << zext48p << zext48p << zext48p;
   Node add6p = nbadd6p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6p), 6);
   NodeBuilder nbadd6x(kind::BITVECTOR_ADD);
   nbadd6x << zext48x << zext48x << zext48x << zext48x;
   Node add6x = nbadd6x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6x), 18);
 
   Node not1p = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(not1p), 40);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1p), 40);
   Node not1x = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(not1x), 40);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1x), 40);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw2)
@@ -2786,7 +2789,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw2)
   Node zext1 = d_nodeManager->mkNode(zextop15, d_p);
   Node ext = bv::utils::mkExtract(zext1, 7, 0);
   Node zext2 = d_nodeManager->mkNode(zextop5, ext);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 4);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
@@ -2805,7 +2808,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
   Node ext2 = bv::utils::mkExtract(z, 4, 0);
   Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
   Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
@@ -2821,7 +2824,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
   Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
   Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
   Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
@@ -2856,7 +2859,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
 
   Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2);
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
@@ -2888,7 +2891,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
 
   Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2);
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
@@ -2994,7 +2997,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww));
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 0);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 0);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
@@ -3098,8 +3101,8 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww));
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 19);
-  ASSERT_EQ(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)), 17);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 19);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(Rewriter::rewrite(plus7)), 17);
 }
 }  // namespace test
 }  // namespace cvc5