Fix BVGauss unit tests. (#3142)

pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the
anonymous namespace, which resulted in ODR (one definition rule)
violations reported by ASAN.

This commit exposes the functionality required in the unit tests as
private static members of the BVGauss class. Since this is a white unit
test, we can access private members in the tests.

1 files changed, 162 insertions, 162 deletions

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index e027fb5e8..7f7af40b9 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -17,8 +17,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "preprocessing/passes/bv_gauss.cpp"
-#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/passes/bv_gauss.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -31,6 +30,7 @@
 
 using namespace CVC4;
 using namespace CVC4::preprocessing;
+using namespace CVC4::preprocessing::passes;
 using namespace CVC4::theory;
 using namespace CVC4::smt;
 
@@ -51,13 +51,13 @@ static void print_matrix_dbg(std::vector<Integer> &rhs,
 static void testGaussElimX(Integer prime,
                            std::vector<Integer> rhs,
                            std::vector<std::vector<Integer>> lhs,
-                           passes::Result expected,
-                           std::vector<Integer> *rrhs = nullptr,
-                           std::vector<std::vector<Integer>> *rlhs = nullptr)
+                           BVGauss::Result expected,
+                           std::vector<Integer>* rrhs = nullptr,
+                           std::vector<std::vector<Integer>>* rlhs = nullptr)
 {
   size_t nrows = lhs.size();
   size_t ncols = lhs[0].size();
-  passes::Result ret;
+  BVGauss::Result ret;
   std::vector<Integer> resrhs = std::vector<Integer>(rhs);
   std::vector<std::vector<Integer>> reslhs =
       std::vector<std::vector<Integer>>(lhs);
@@ -65,21 +65,21 @@ static void testGaussElimX(Integer prime,
   std::cout << "Input: " << std::endl;
   print_matrix_dbg(rhs, lhs);
 
-  ret = passes::gaussElim(prime, resrhs, reslhs);
+  ret = BVGauss::gaussElim(prime, resrhs, reslhs);
 
-  std::cout << "passes::Result: "
-            << (ret == passes::Result::INVALID
+  std::cout << "BVGauss::Result: "
+            << (ret == BVGauss::Result::INVALID
                     ? "INVALID"
-                    : (ret == passes::Result::UNIQUE
+                    : (ret == BVGauss::Result::UNIQUE
                            ? "UNIQUE"
-                           : (ret == passes::Result::PARTIAL ? "PARTIAL"
-                                                                  : "NONE")))
+                           : (ret == BVGauss::Result::PARTIAL ? "PARTIAL"
+                                                              : "NONE")))
             << std::endl;
   print_matrix_dbg(resrhs, reslhs);
 
   TS_ASSERT_EQUALS(expected, ret);
 
-  if (expected == passes::Result::UNIQUE)
+  if (expected == BVGauss::Result::UNIQUE)
   {
     /* map result value to column index
      * e.g.:
@@ -121,7 +121,7 @@ static void testGaussElimT(Integer prime,
                            std::vector<Integer> rhs,
                            std::vector<std::vector<Integer>> lhs)
 {
-  TS_ASSERT_THROWS(passes::gaussElim(prime, rhs, lhs), T);
+  TS_ASSERT_THROWS(BVGauss::gaussElim(prime, rhs, lhs), T);
 }
 
 class TheoryBVGaussWhite : public CxxTest::TestSuite
@@ -321,27 +321,27 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     std::cout << "matrix 0, modulo 0" << std::endl;  // throws
     testGaussElimT<AssertionException>(Integer(0), rhs, lhs);
     std::cout << "matrix 0, modulo 1" << std::endl;
-    testGaussElimX(Integer(1), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 2" << std::endl;
-    testGaussElimX(Integer(2), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(2), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 3" << std::endl;
-    testGaussElimX(Integer(3), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(3), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 4" << std::endl;  // no inverse
-    testGaussElimX(Integer(4), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(4), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 5" << std::endl;
-    testGaussElimX(Integer(5), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(5), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 6" << std::endl;  // no inverse
-    testGaussElimX(Integer(6), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(6), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 8" << std::endl;  // no inverse
-    testGaussElimX(Integer(8), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(8), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 9" << std::endl;
-    testGaussElimX(Integer(9), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 10" << std::endl;  // no inverse
-    testGaussElimX(Integer(10), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(10), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueDone()
@@ -361,7 +361,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(1), Integer(0)},
            {Integer(0), Integer(0), Integer(1)}};
     std::cout << "matrix 1, modulo 17" << std::endl;
-    testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(17), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUnique()
@@ -381,11 +381,11 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(4), Integer(5), Integer(6)},
            {Integer(3), Integer(1), Integer(-2)}};
     std::cout << "matrix 2, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 2, modulo 17" << std::endl;
-    testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(17), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 2, modulo 59" << std::endl;
-    testGaussElimX(Integer(59), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(59), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *      lhs       rhs         lhs     rhs   modulo 11
@@ -401,7 +401,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(1), Integer(-1), Integer(-1), Integer(-2)},
            {Integer(2), Integer(-1), Integer(2), Integer(-1)}};
     std::cout << "matrix 3, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero1()
@@ -421,7 +421,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(1), Integer(1), Integer(1)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 4, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -435,7 +435,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(4), Integer(5)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 5, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -449,7 +449,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(3), Integer(2), Integer(5)},
            {Integer(0), Integer(4), Integer(5)}};
     std::cout << "matrix 6, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero2()
@@ -469,7 +469,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(1), Integer(1), Integer(1)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 7, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -483,7 +483,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(5)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 8, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -497,7 +497,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(3), Integer(2), Integer(5)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 9, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero3()
@@ -517,7 +517,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(0), Integer(6)}};
     std::cout << "matrix 10, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 7
@@ -531,7 +531,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(6), Integer(0)}};
     std::cout << "matrix 11, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero4()
@@ -551,7 +551,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 12, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -565,7 +565,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(3), Integer(5)},
            {Integer(0), Integer(0), Integer(0)}};
     std::cout << "matrix 13, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -579,7 +579,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(3), Integer(5)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 14, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -593,7 +593,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 15, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -607,7 +607,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(0), Integer(5)},
            {Integer(0), Integer(0), Integer(0)}};
     std::cout << "matrix 16, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -621,7 +621,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(0), Integer(5)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 17, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -635,7 +635,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(0), Integer(0)}};
     std::cout << "matrix 18, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -649,7 +649,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(0)},
            {Integer(0), Integer(0), Integer(0)}};
     std::cout << "matrix 18, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -663,7 +663,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(0)},
            {Integer(4), Integer(0), Integer(0)}};
     std::cout << "matrix 19, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs  modulo 2
@@ -682,7 +682,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
               {Integer(0), Integer(0), Integer(0)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(2), rhs, lhs, passes::Result::UNIQUE, &resrhs, &reslhs);
+        Integer(2), rhs, lhs, BVGauss::Result::UNIQUE, &resrhs, &reslhs);
   }
 
   void testGaussElimUniquePartial()
@@ -700,7 +700,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(2), Integer(0), Integer(6)},
            {Integer(4), Integer(0), Integer(6)}};
     std::cout << "matrix 21, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 7
@@ -712,7 +712,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(2), Integer(6), Integer(0)},
            {Integer(4), Integer(6), Integer(0)}};
     std::cout << "matrix 22, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimNone()
@@ -732,7 +732,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(4), Integer(5), Integer(6)},
            {Integer(3), Integer(1), Integer(-2)}};
     std::cout << "matrix 23, modulo 9" << std::endl;
-    testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::INVALID);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs       modulo 59
@@ -746,7 +746,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(4), Integer(12)},
            {Integer(1), Integer(-4), Integer(-12)}};
     std::cout << "matrix 24, modulo 59" << std::endl;
-    testGaussElimX(Integer(59), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(59), rhs, lhs, BVGauss::Result::NONE);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs       modulo 9
@@ -760,7 +760,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(4), Integer(5), Integer(6)},
            {Integer(2), Integer(7), Integer(12)}};
     std::cout << "matrix 25, modulo 9" << std::endl;
-    testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::INVALID);
   }
 
   void testGaussElimNoneZero()
@@ -780,7 +780,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(3), Integer(5)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 26, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -794,7 +794,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(0), Integer(5)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 27, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -808,7 +808,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(0)},
            {Integer(4), Integer(0), Integer(0)}};
     std::cout << "matrix 28, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
   }
 
   void testGaussElimPartial1()
@@ -826,7 +826,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(1), Integer(0), Integer(9)},
            {Integer(0), Integer(1), Integer(3)}};
     std::cout << "matrix 29, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -838,7 +838,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(1), Integer(3), Integer(0)},
            {Integer(0), Integer(0), Integer(1)}};
     std::cout << "matrix 30, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -850,7 +850,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(1), Integer(1), Integer(1)},
            {Integer(2), Integer(3), Integer(5)}};
     std::cout << "matrix 31, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs  modulo { 3, 5, 7, 11, 17, 31, 59 }
@@ -869,38 +869,38 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
               {Integer(0), Integer(0), Integer(0)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(3), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     resrhs = {Integer(1), Integer(4), Integer(0)};
     std::cout << "matrix 32, modulo 5" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(4)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(5), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(5), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 7" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(6)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(7), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(7), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 11" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(10)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(11), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(11), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 17" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(16)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(17), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(17), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 59" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(58)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(59), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(59), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs        lhs   rhs   modulo 3
@@ -919,7 +919,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
               {Integer(0), Integer(0), Integer(0)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(3), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
   }
 
   void testGaussElimPartial2()
@@ -940,7 +940,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(2), Integer(2)},
            {Integer(0), Integer(0), Integer(1), Integer(0)}};
     std::cout << "matrix 34, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
   }
   void testGaussElimRewriteForUremUnique1()
   {
@@ -984,8 +984,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
     TS_ASSERT(res[d_x] == d_three32);
     TS_ASSERT(res[d_y] == d_four32);
@@ -1083,8 +1083,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
     TS_ASSERT(res[d_x] == d_three32);
     TS_ASSERT(res[d_y] == d_four32);
@@ -1094,7 +1094,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial1()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1120,8 +1120,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1212,7 +1212,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial1a()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1236,8 +1236,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1328,7 +1328,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial2()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1351,8 +1351,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
                      d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1414,7 +1414,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial3()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1445,8 +1445,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_eight);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1535,7 +1535,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial4()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *     lhs    rhs          lhs    rhs  modulo 11
@@ -1579,8 +1579,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_thirty);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1677,7 +1677,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial5()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *     lhs    rhs         lhs   rhs  modulo 3
@@ -1721,8 +1721,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_thirty);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 1);
 
     Node x1 = d_nm->mkNode(kind::BITVECTOR_UREM,
@@ -1784,7 +1784,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial6()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *    lhs    rhs  -->    lhs    rhs  modulo 11
@@ -1828,8 +1828,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_two);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 3);
 
     Node x1 = d_nm->mkNode(
@@ -1872,7 +1872,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremWithExprPartial()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1919,8 +1919,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     x = Rewriter::rewrite(x);
@@ -2015,7 +2015,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremNAryPartial()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -2082,8 +2082,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
                             d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     x_mul_xx = Rewriter::rewrite(x_mul_xx);
@@ -2178,7 +2178,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremNotInvalid1()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      * 3x / 2z = 4  modulo 11
@@ -2208,8 +2208,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n3, d_p), d_five);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
 
     TS_ASSERT(res[n1] == d_four32);
@@ -2220,7 +2220,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremNotInvalid2()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      * x*y = 4  modulo 11
@@ -2267,8 +2267,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         bv::utils::mkConcat(d_zero, d_nine));
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
 
     n1 = Rewriter::rewrite(n1);
@@ -2289,7 +2289,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremInvalid()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      * x*y = 4  modulo 11
@@ -2332,8 +2332,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         bv::utils::mkConcat(d_zero, d_nine));
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::INVALID);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::INVALID);
   }
 
   void testGaussElimRewriteUnique1()
@@ -2590,15 +2590,15 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
   void testGetMinBw1()
   {
-    TS_ASSERT(passes::getMinBwExpr(bv::utils::mkConst(32, 11)) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(bv::utils::mkConst(32, 11)) == 4);
 
-    TS_ASSERT(passes::getMinBwExpr(d_p) == 4);
-    TS_ASSERT(passes::getMinBwExpr(d_x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(d_p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(d_x) == 16);
 
     Node extp = bv::utils::mkExtract(d_p, 4, 0);
-    TS_ASSERT(passes::getMinBwExpr(extp) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(extp) == 4);
     Node extx = bv::utils::mkExtract(d_x, 4, 0);
-    TS_ASSERT(passes::getMinBwExpr(extx) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(extx) == 5);
 
     Node zextop8 = d_nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(8));
     Node zextop16 = d_nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(16));
@@ -2606,132 +2606,132 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node zextop40 = d_nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(40));
 
     Node zext40p = d_nm->mkNode(zextop8, d_p);
-    TS_ASSERT(passes::getMinBwExpr(zext40p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext40p) == 4);
     Node zext40x = d_nm->mkNode(zextop8, d_x);
-    TS_ASSERT(passes::getMinBwExpr(zext40x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext40x) == 16);
 
     Node zext48p = d_nm->mkNode(zextop16, d_p);
-    TS_ASSERT(passes::getMinBwExpr(zext48p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48p) == 4);
     Node zext48x = d_nm->mkNode(zextop16, d_x);
-    TS_ASSERT(passes::getMinBwExpr(zext48x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48x) == 16);
 
     Node p8 = d_nm->mkConst<BitVector>(BitVector(8, 11u));
     Node x8 = d_nm->mkVar("x8", d_nm->mkBitVectorType(8));
 
     Node zext48p8 = d_nm->mkNode(zextop40, p8);
-    TS_ASSERT(passes::getMinBwExpr(zext48p8) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48p8) == 4);
     Node zext48x8 = d_nm->mkNode(zextop40, x8);
-    TS_ASSERT(passes::getMinBwExpr(zext48x8) == 8);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48x8) == 8);
 
     Node mult1p = d_nm->mkNode(kind::BITVECTOR_MULT, extp, extp);
-    TS_ASSERT(passes::getMinBwExpr(mult1p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult1p) == 5);
     Node mult1x = d_nm->mkNode(kind::BITVECTOR_MULT, extx, extx);
-    TS_ASSERT(passes::getMinBwExpr(mult1x) == 0);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult1x) == 0);
 
     Node mult2p = d_nm->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p);
-    TS_ASSERT(passes::getMinBwExpr(mult2p) == 7);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult2p) == 7);
     Node mult2x = d_nm->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x);
-    TS_ASSERT(passes::getMinBwExpr(mult2x) == 32);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult2x) == 32);
 
     NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT);
     nbmult3p << zext48p << zext48p << zext48p;
     Node mult3p = nbmult3p;
-    TS_ASSERT(passes::getMinBwExpr(mult3p) == 11);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult3p) == 11);
     NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT);
     nbmult3x << zext48x << zext48x << zext48x;
     Node mult3x = nbmult3x;
-    TS_ASSERT(passes::getMinBwExpr(mult3x) == 48);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult3x) == 48);
 
     NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT);
     nbmult4p << zext48p  << zext48p8 << zext48p;
     Node mult4p = nbmult4p;
-    TS_ASSERT(passes::getMinBwExpr(mult4p) == 11);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult4p) == 11);
     NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT);
     nbmult4x << zext48x  << zext48x8 << zext48x;
     Node mult4x = nbmult4x;
-    TS_ASSERT(passes::getMinBwExpr(mult4x) == 40);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult4x) == 40);
 
     Node concat1p = bv::utils::mkConcat(d_p, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(concat1p) == 52);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat1p) == 52);
     Node concat1x = bv::utils::mkConcat(d_x, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(concat1x) == 64);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat1x) == 64);
 
     Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p);
-    TS_ASSERT(passes::getMinBwExpr(concat2p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat2p) == 4);
     Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x);
-    TS_ASSERT(passes::getMinBwExpr(concat2x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat2x) == 16);
 
     Node udiv1p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(udiv1p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv1p) == 1);
     Node udiv1x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(udiv1x) == 48);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv1x) == 48);
 
     Node udiv2p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8);
-    TS_ASSERT(passes::getMinBwExpr(udiv2p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv2p) == 1);
     Node udiv2x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8);
-    TS_ASSERT(passes::getMinBwExpr(udiv2x) == 48);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv2x) == 48);
 
     Node urem1p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(urem1p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem1p) == 1);
     Node urem1x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(urem1x) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem1x) == 1);
 
     Node urem2p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8);
-    TS_ASSERT(passes::getMinBwExpr(urem2p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem2p) == 1);
     Node urem2x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8);
-    TS_ASSERT(passes::getMinBwExpr(urem2x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem2x) == 16);
 
     Node urem3p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(urem3p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem3p) == 1);
     Node urem3x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(urem3x) == 8);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem3x) == 8);
 
     Node add1p = d_nm->mkNode(kind::BITVECTOR_PLUS, extp, extp);
-    TS_ASSERT(passes::getMinBwExpr(add1p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(add1p) == 5);
     Node add1x = d_nm->mkNode(kind::BITVECTOR_PLUS, extx, extx);
-    TS_ASSERT(passes::getMinBwExpr(add1x) == 0);
+    TS_ASSERT(BVGauss::getMinBwExpr(add1x) == 0);
 
     Node add2p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p);
-    TS_ASSERT(passes::getMinBwExpr(add2p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(add2p) == 5);
     Node add2x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x);
-    TS_ASSERT(passes::getMinBwExpr(add2x) == 17);
+    TS_ASSERT(BVGauss::getMinBwExpr(add2x) == 17);
 
     Node add3p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(add3p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(add3p) == 5);
     Node add3x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(add3x) == 17);
+    TS_ASSERT(BVGauss::getMinBwExpr(add3x) == 17);
 
     NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS);
     nbadd4p << zext48p << zext48p << zext48p;
     Node add4p = nbadd4p;
-    TS_ASSERT(passes::getMinBwExpr(add4p) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(add4p) == 6);
     NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS);
     nbadd4x << zext48x << zext48x << zext48x;
     Node add4x = nbadd4x;
-    TS_ASSERT(passes::getMinBwExpr(add4x) == 18);
+    TS_ASSERT(BVGauss::getMinBwExpr(add4x) == 18);
 
     NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS);
     nbadd5p << zext48p << zext48p8 << zext48p;
     Node add5p = nbadd5p;
-    TS_ASSERT(passes::getMinBwExpr(add5p) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(add5p) == 6);
     NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS);
     nbadd5x << zext48x << zext48x8 << zext48x;
     Node add5x = nbadd5x;
-    TS_ASSERT(passes::getMinBwExpr(add5x) == 18);
+    TS_ASSERT(BVGauss::getMinBwExpr(add5x) == 18);
 
     NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS);
     nbadd6p << zext48p << zext48p << zext48p << zext48p;
     Node add6p = nbadd6p;
-    TS_ASSERT(passes::getMinBwExpr(add6p) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(add6p) == 6);
     NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS);
     nbadd6x << zext48x << zext48x << zext48x << zext48x;
     Node add6x = nbadd6x;
-    TS_ASSERT(passes::getMinBwExpr(add6x) == 18);
+    TS_ASSERT(BVGauss::getMinBwExpr(add6x) == 18);
 
     Node not1p = d_nm->mkNode(kind::BITVECTOR_NOT, zext40p);
-    TS_ASSERT(passes::getMinBwExpr(not1p) == 40);
+    TS_ASSERT(BVGauss::getMinBwExpr(not1p) == 40);
     Node not1x = d_nm->mkNode(kind::BITVECTOR_NOT, zext40x);
-    TS_ASSERT(passes::getMinBwExpr(not1x) == 40);
+    TS_ASSERT(BVGauss::getMinBwExpr(not1x) == 40);
   }
 
   void testGetMinBw2()
@@ -2743,7 +2743,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node zext1 = d_nm->mkNode(zextop15, d_p);
     Node ext = bv::utils::mkExtract(zext1, 7, 0);
     Node zext2 = d_nm->mkNode(zextop5, ext);
-    TS_ASSERT(passes::getMinBwExpr(zext2) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext2) == 4);
   }
 
   void testGetMinBw3a()
@@ -2761,7 +2761,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node ext2 = bv::utils::mkExtract(z, 4, 0);
     Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2);
     Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-    TS_ASSERT(passes::getMinBwExpr(zext2) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext2) == 5);
   }
 
   void testGetMinBw3b()
@@ -2776,7 +2776,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
     Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2);
     Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-    TS_ASSERT(passes::getMinBwExpr(zext2) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext2) == 5);
   }
 
   void testGetMinBw4a()
@@ -2809,7 +2809,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
 
-    TS_ASSERT(passes::getMinBwExpr(plus) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus) == 6);
   }
 
   void testGetMinBw4b()
@@ -2839,7 +2839,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
 
-    TS_ASSERT(passes::getMinBwExpr(plus) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus) == 6);
   }
 
   void testGetMinBw5a()
@@ -2935,7 +2935,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         plus6,
         d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww));
 
-    TS_ASSERT(passes::getMinBwExpr(plus7) == 0);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus7) == 0);
   }
 
   void testGetMinBw5b()
@@ -3030,8 +3030,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         plus6,
         d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww));
 
-    TS_ASSERT(passes::getMinBwExpr(plus7) == 19);
-    TS_ASSERT(passes::getMinBwExpr(Rewriter::rewrite(plus7)) == 17);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus7) == 19);
+    TS_ASSERT(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)) == 17);
   }
 
 };