BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

4 files changed, 156 insertions, 158 deletions

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 839b516e4..a8c1fae25 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -895,9 +895,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one),
+                  kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one),
               d_z_mul_one),
           d_p),
       d_five);
@@ -907,9 +907,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
               d_z_mul_five),
           d_p),
       d_eight);
@@ -919,7 +919,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five),
+              kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five),
           d_p),
       d_two);
 
@@ -949,7 +949,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
   Node p = d_nodeManager->mkNode(
       zextop6,
       bv::utils::mkConcat(bv::utils::mkZero(6),
-                          d_nodeManager->mkNode(kind::BITVECTOR_PLUS,
+                          d_nodeManager->mkNode(kind::BITVECTOR_ADD,
                                                 bv::utils::mkConst(20, 7),
                                                 bv::utils::mkConst(20, 4))));
 
@@ -980,7 +980,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       bv::utils::mkExtract(
           d_nodeManager->mkNode(
               zextop6,
-              d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_three, d_two)),
+              d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_three, d_two)),
           31,
           0),
       d_z);
@@ -990,7 +990,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UDIV,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT,
                                     bv::utils::mkConst(32, 4),
                                     bv::utils::mkConst(32, 5)),
@@ -1003,8 +1003,8 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
-              d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_one, y_mul_one),
+              kind::BITVECTOR_ADD,
+              d_nodeManager->mkNode(kind::BITVECTOR_ADD, x_mul_one, y_mul_one),
               z_mul_one),
           p),
       d_five);
@@ -1014,9 +1014,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, x_mul_two, y_mul_three),
+                  kind::BITVECTOR_ADD, x_mul_two, y_mul_three),
               z_mul_five),
           p),
       d_eight);
@@ -1025,7 +1025,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_four, z_mul_five),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, x_mul_four, z_mul_five),
           d_p),
       d_two);
 
@@ -1055,8 +1055,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_one, d_z_mul_nine),
           d_p),
       d_seven);
 
@@ -1065,7 +1064,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three),
+              kind::BITVECTOR_ADD, d_y_mul_one, d_z_mul_three),
           d_p),
       d_nine);
 
@@ -1077,14 +1076,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_seven32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
       d_p);
   Node y1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_nine32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
       d_p);
@@ -1092,14 +1091,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
   Node x2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
       d_p);
   Node z2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
       d_p);
@@ -1107,14 +1106,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
   Node y3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
       d_p);
   Node z3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
       d_p);
@@ -1181,7 +1180,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x, d_z_mul_nine),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x, d_z_mul_nine),
           d_p),
       d_seven);
 
@@ -1189,7 +1188,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_y, d_z_mul_three),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_y, d_z_mul_three),
           d_p),
       d_nine);
 
@@ -1201,14 +1200,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_seven32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
       d_p);
   Node y1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_nine32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
       d_p);
@@ -1216,14 +1215,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
   Node x2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
       d_p);
   Node z2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
       d_p);
@@ -1231,14 +1230,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
   Node y3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
       d_p);
   Node z3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
       d_p);
@@ -1306,7 +1305,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_three),
+              kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_three),
           d_p),
       d_seven);
 
@@ -1323,14 +1322,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_seven32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_eight32)),
       d_p);
   Node y2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_six32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_seven32)),
       d_p);
@@ -1395,8 +1394,8 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
-              d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y),
+              kind::BITVECTOR_ADD,
+              d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_one, d_y),
               d_z_mul_one),
           d_p),
       d_five);
@@ -1406,9 +1405,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
               d_z_mul_five),
           d_p),
       d_eight);
@@ -1421,42 +1420,42 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_seven32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
       d_p);
   Node y1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_nine32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
       d_p);
   Node x2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
       d_p);
   Node z2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
       d_p);
   Node y3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
       d_p);
   Node z3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
       d_p);
@@ -1525,9 +1524,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_four),
               d_z_mul_six),
           d_p),
       d_eighteen);
@@ -1537,9 +1536,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five),
+                  kind::BITVECTOR_ADD, d_x_mul_four, d_y_mul_five),
               d_z_mul_six),
           d_p),
       d_twentyfour);
@@ -1549,9 +1548,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_seven),
               d_z_mul_twelve),
           d_p),
       d_thirty);
@@ -1564,42 +1563,42 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_one32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_one32)),
       d_p);
   Node y1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_four32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_nine32)),
       d_p);
   Node x2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)),
       d_p);
   Node z2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)),
       d_p);
   Node y3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_six32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_nine32)),
       d_p);
   Node z3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_ten32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_one32)),
       d_p);
@@ -1676,9 +1675,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_four),
               d_z_mul_six),
           d_three),
       d_eighteen);
@@ -1688,9 +1687,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five),
+                  kind::BITVECTOR_ADD, d_x_mul_four, d_y_mul_five),
               d_z_mul_six),
           d_three),
       d_twentyfour);
@@ -1700,9 +1699,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_seven),
               d_z_mul_twelve),
           d_three),
       d_thirty);
@@ -1796,9 +1795,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_one, y_mul_two),
+                  kind::BITVECTOR_ADD, d_x_mul_one, y_mul_two),
               w_mul_six),
           d_p),
       d_two);
@@ -1807,7 +1806,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, z_mul_two, w_mul_two),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, z_mul_two, w_mul_two),
           d_p),
       d_two);
 
@@ -1822,7 +1821,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_one32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_nine32)),
       d_p);
@@ -1832,7 +1831,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
   Node y2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_six32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_five32)),
       d_p);
@@ -1897,7 +1896,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_one, nine_mul_z),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, x_mul_one, nine_mul_z),
           d_p),
       d_seven);
 
@@ -1905,7 +1904,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, one_mul_y, z_mul_three),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, one_mul_y, z_mul_three),
           d_p),
       d_nine);
 
@@ -1921,14 +1920,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_seven32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_two32)),
       d_p);
   Node y1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_nine32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_eight32)),
       d_p);
@@ -1936,14 +1935,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
   Node x2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, y, d_three32)),
       d_p);
   Node z2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, y, d_seven32)),
       d_p);
@@ -1951,14 +1950,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
   Node y3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_four32)),
       d_p);
   Node z3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_six32)),
       d_p);
@@ -2067,7 +2066,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, x_mul_one_mul_xx, z_mul_nine_mul_zz),
+              kind::BITVECTOR_ADD, x_mul_one_mul_xx, z_mul_nine_mul_zz),
           d_p),
       d_seven);
 
@@ -2076,7 +2075,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, y_mul_yy_mul_one, three_mul_z_mul_zz),
+              kind::BITVECTOR_ADD, y_mul_yy_mul_one, three_mul_z_mul_zz),
           d_p),
       d_nine);
 
@@ -2092,14 +2091,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
   Node x1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_seven32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_two32)),
       d_p);
   Node y1 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_nine32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_eight32)),
       d_p);
@@ -2107,14 +2106,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
   Node x2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_three32)),
       d_p);
   Node z2 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_seven32)),
       d_p);
@@ -2122,14 +2121,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
   Node y3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_three32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_four32)),
       d_p);
   Node z3 = d_nodeManager->mkNode(
       kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_PLUS,
+          kind::BITVECTOR_ADD,
           d_two32,
           d_nodeManager->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_six32)),
       d_p);
@@ -2254,7 +2253,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
                             d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y),
                             z);
   Node n3 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       d_nodeManager->mkNode(kind::BITVECTOR_MULT,
                             d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y),
                             bv::utils::mkConcat(d_zero, d_two)),
@@ -2367,9 +2366,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one),
+                  kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one),
               d_z_mul_one),
           d_p),
       d_five);
@@ -2379,9 +2378,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
               d_z_mul_five),
           d_p),
       d_eight);
@@ -2391,7 +2390,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five),
+              kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five),
           d_p),
       d_two);
 
@@ -2436,9 +2435,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one),
+                  kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one),
               d_z_mul_one),
           d_p),
       d_five);
@@ -2448,9 +2447,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nodeManager->mkNode(
-                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
+                  kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
               d_z_mul_five),
           d_p),
       d_eight);
@@ -2460,7 +2459,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five),
+              kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five),
           d_p),
       d_two);
 
@@ -2470,7 +2469,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, y_mul_six),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_two, y_mul_six),
           d_seven),
       d_four);
 
@@ -2478,7 +2477,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, y_mul_six),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_four, y_mul_six),
           d_seven),
       d_three);
 
@@ -2524,8 +2523,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       kind::EQUAL,
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
-          d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine),
+          d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_one, d_z_mul_nine),
           d_p),
       d_seven);
 
@@ -2534,7 +2532,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three),
+              kind::BITVECTOR_ADD, d_y_mul_one, d_z_mul_three),
           d_p),
       d_nine);
 
@@ -2553,7 +2551,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_seven32,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
           d_p));
@@ -2563,7 +2561,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_nine32,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
           d_p));
@@ -2574,7 +2572,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_two32,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
           d_p));
@@ -2584,7 +2582,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_three32,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
           d_p));
@@ -2595,7 +2593,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_three32,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
           d_p));
@@ -2605,7 +2603,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
       d_nodeManager->mkNode(
           kind::BITVECTOR_UREM,
           d_nodeManager->mkNode(
-              kind::BITVECTOR_PLUS,
+              kind::BITVECTOR_ADD,
               d_two32,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
           d_p));
@@ -2723,44 +2721,44 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1)
   Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8);
 
-  Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extp, extp);
+  Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extp, extp);
   ASSERT_EQ(BVGauss::getMinBwExpr(add1p), 5);
-  Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extx, extx);
+  Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extx, extx);
   ASSERT_EQ(BVGauss::getMinBwExpr(add1x), 0);
 
-  Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p);
+  Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40p, zext40p);
   ASSERT_EQ(BVGauss::getMinBwExpr(add2p), 5);
-  Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x);
+  Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40x, zext40x);
   ASSERT_EQ(BVGauss::getMinBwExpr(add2x), 17);
 
-  Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p);
+  Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48p8, zext48p);
   ASSERT_EQ(BVGauss::getMinBwExpr(add3p), 5);
-  Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x);
+  Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48x8, zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17);
 
-  NodeBuilder nbadd4p(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd4p(kind::BITVECTOR_ADD);
   nbadd4p << zext48p << zext48p << zext48p;
   Node add4p = nbadd4p;
   ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6);
-  NodeBuilder nbadd4x(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd4x(kind::BITVECTOR_ADD);
   nbadd4x << zext48x << zext48x << zext48x;
   Node add4x = nbadd4x;
   ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18);
 
-  NodeBuilder nbadd5p(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd5p(kind::BITVECTOR_ADD);
   nbadd5p << zext48p << zext48p8 << zext48p;
   Node add5p = nbadd5p;
   ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6);
-  NodeBuilder nbadd5x(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd5x(kind::BITVECTOR_ADD);
   nbadd5x << zext48x << zext48x8 << zext48x;
   Node add5x = nbadd5x;
   ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18);
 
-  NodeBuilder nbadd6p(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd6p(kind::BITVECTOR_ADD);
   nbadd6p << zext48p << zext48p << zext48p << zext48p;
   Node add6p = nbadd6p;
   ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6);
-  NodeBuilder nbadd6x(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd6x(kind::BITVECTOR_ADD);
   nbadd6x << zext48x << zext48x << zext48x << zext48x;
   Node add6x = nbadd6x;
   ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18);
@@ -2850,7 +2848,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
   Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2);
   Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
 
-  Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
+  Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2);
 
   ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
 }
@@ -2882,7 +2880,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
   Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2);
   Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
 
-  Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
+  Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2);
 
   ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
 }
@@ -2954,38 +2952,38 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
   Node s15 = bv::utils::mkConcat(bv::utils::mkZero(5), ext15s);
 
   Node plus1 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 86), xx),
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 41), yy));
   Node plus2 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus1,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 37), zz));
   Node plus3 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus2,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 170), uu));
   Node plus4 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus3,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 112), uu));
   Node plus5 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus4,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 195), s15));
   Node plus6 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus5,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 124), s7));
   Node plus7 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus6,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww));
@@ -3058,38 +3056,38 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
   Node s15 = bv::utils::mkConcat(bv::utils::mkZero(12), ext15s);
 
   Node plus1 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 86), xx),
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 41), yy));
   Node plus2 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus1,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 37), zz));
   Node plus3 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus2,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 170), uu));
   Node plus4 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus3,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 112), uu));
   Node plus5 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus4,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 195), s15));
   Node plus6 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus5,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 124), s7));
   Node plus7 = d_nodeManager->mkNode(
-      kind::BITVECTOR_PLUS,
+      kind::BITVECTOR_ADD,
       plus6,
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww));
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index bfdcfb604..094a32772 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -58,7 +58,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
 
   Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
   Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
-  Node x_plus_y = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x, y);
+  Node x_plus_y = d_nodeManager->mkNode(kind::BITVECTOR_ADD, x, y);
   Node one = d_nodeManager->mkConst<BitVector>(BitVector(16, 1u));
   Node x_shl_one = d_nodeManager->mkNode(kind::BITVECTOR_SHL, x, one);
   Node eq = d_nodeManager->mkNode(kind::EQUAL, x_plus_y, x_shl_one);
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
index 85f14b245..6c336afd4 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
@@ -50,12 +50,12 @@ class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt
 
   Node mkPlus(TNode a, TNode b)
   {
-    return d_nodeManager->mkNode(kind::BITVECTOR_PLUS, a, b);
+    return d_nodeManager->mkNode(kind::BITVECTOR_ADD, a, b);
   }
 
   Node mkPlus(const std::vector<Node>& children)
   {
-    return d_nodeManager->mkNode(kind::BITVECTOR_PLUS, children);
+    return d_nodeManager->mkNode(kind::BITVECTOR_ADD, children);
   }
 };
 
@@ -230,7 +230,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_xa = normalizePvPlus(x, {x, a}, contains_x);
   ASSERT_TRUE(contains_x[norm_xa]);
   ASSERT_TRUE(norm_xa.getAttribute(is_linear));
-  ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_xa.getNumChildren(), 2);
   ASSERT_EQ(norm_xa[0], x);
   ASSERT_EQ(norm_xa[1], a);
@@ -239,7 +239,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_ax = normalizePvPlus(x, {a, x}, contains_x);
   ASSERT_TRUE(contains_x[norm_ax]);
   ASSERT_TRUE(norm_ax.getAttribute(is_linear));
-  ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_ax.getNumChildren(), 2);
   ASSERT_EQ(norm_ax[0], x);
   ASSERT_EQ(norm_ax[1], a);
@@ -248,7 +248,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_neg_ax = normalizePvPlus(x, {a, neg_x}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_ax]);
   ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear));
-  ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_neg_ax.getNumChildren(), 2);
   ASSERT_EQ(norm_neg_ax[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_ax[0].getNumChildren(), 2);
@@ -272,7 +272,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_abcxd = normalizePvPlus(x, {a, b, c, x, d}, contains_x);
   ASSERT_TRUE(contains_x[norm_abcxd]);
   ASSERT_TRUE(norm_abcxd.getAttribute(is_linear));
-  ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_abcxd.getNumChildren(), 2);
   ASSERT_EQ(norm_abcxd[0], x);
   ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d})));
@@ -281,7 +281,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_neg_abcxd = normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_abcxd]);
   ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear));
-  ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_neg_abcxd.getNumChildren(), 2);
   ASSERT_EQ(norm_neg_abcxd[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_abcxd[0].getNumChildren(), 2);
@@ -295,7 +295,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_bxa = normalizePvPlus(x, {b, norm_ax}, contains_x);
   ASSERT_TRUE(contains_x[norm_bxa]);
   ASSERT_TRUE(norm_bxa.getAttribute(is_linear));
-  ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_bxa.getNumChildren(), 2);
   ASSERT_EQ(norm_bxa[0], x);
   ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkPlus(b, a)));
@@ -306,7 +306,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node norm_neg_bxa = normalizePvPlus(x, {b, neg_norm_ax}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_bxa]);
   ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear));
-  ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_PLUS);
+  ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_neg_bxa.getNumChildren(), 2);
   ASSERT_EQ(norm_neg_abcxd[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_abcxd[0].getNumChildren(), 2);
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index 83d982d8e..e5ba92995 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -696,97 +696,97 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_sgt_false1)
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_true0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_true1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_false0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_false1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_true0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_true1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_false0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_false1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_true0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_true1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_false0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_false1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_true0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_true1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_false0)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s);
   runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_false1)
 {
-  Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x);
+  Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x);
   runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt);
 }