From 9670dd43576cd21de82e22e76c57e783aa143d21 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 20 May 2021 17:41:50 -0700
Subject: [PATCH] BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

---
 examples/api/bitvectors.cpp                   |   2 +-
 examples/api/java/BitVectors.java             |   2 +-
 examples/api/python/bitvectors.py             |   2 +-
 src/api/cpp/cvc5.cpp                          |   4 +-
 src/api/cpp/cvc5_kind.h                       |   7 +-
 src/api/parsekinds.py                         |   2 +-
 src/expr/proof_rule.cpp                       |   2 +-
 src/expr/proof_rule.h                         |   2 +-
 src/parser/cvc/Cvc.g                          |   2 +-
 src/parser/smt2/smt2.cpp                      |   2 +-
 src/preprocessing/passes/bv_gauss.cpp         |  19 +-
 src/preprocessing/passes/bv_to_int.cpp        |   6 +-
 src/preprocessing/passes/int_to_bv.cpp        |   2 +-
 .../passes/unconstrained_simplifier.cpp       |   2 +-
 src/printer/cvc/cvc_printer.cpp               |   5 +-
 src/printer/smt2/smt2_printer.cpp             |   7 +-
 src/smt_util/nary_builder.cpp                 |   2 +-
 .../bitblast/bitblast_strategies_template.h   |   9 +-
 src/theory/bv/bitblast/bitblaster.h           |   2 +-
 src/theory/bv/bitblast/proof_bitblaster.cpp   |   2 +-
 src/theory/bv/bv_solver_lazy.cpp              |  26 +-
 src/theory/bv/bv_subtheory_core.cpp           |   2 +-
 src/theory/bv/bv_subtheory_inequality.cpp     |   2 +-
 src/theory/bv/kinds                           |   4 +-
 src/theory/bv/proof_checker.cpp               |   4 +-
 src/theory/bv/theory_bv.cpp                   |   2 +-
 src/theory/bv/theory_bv_rewrite_rules.h       |  40 +--
 ...ory_bv_rewrite_rules_constant_evaluation.h |  15 +-
 .../theory_bv_rewrite_rules_normalization.h   | 106 +++----
 ...ry_bv_rewrite_rules_operator_elimination.h |  19 +-
 .../theory_bv_rewrite_rules_simplification.h  |  43 +--
 src/theory/bv/theory_bv_rewriter.cpp          |  29 +-
 src/theory/bv/theory_bv_rewriter.h            |   2 +-
 src/theory/bv/theory_bv_utils.cpp             |   2 +-
 src/theory/bv/theory_bv_utils.h               |   2 +-
 src/theory/datatypes/sygus_simple_sym.cpp     |   4 +-
 src/theory/evaluator.cpp                      |   2 +-
 src/theory/fp/fp_converter.cpp                |   4 +-
 src/theory/quantifiers/bv_inverter.cpp        |   4 +-
 src/theory/quantifiers/bv_inverter_utils.cpp  |   6 +-
 .../quantifiers/cegqi/ceg_bv_instantiator.cpp |   6 +-
 .../cegqi/ceg_bv_instantiator_utils.cpp       |  10 +-
 .../cegqi/ceg_bv_instantiator_utils.h         |   2 +-
 src/theory/quantifiers/extended_rewrite.h     |   4 +-
 .../quantifiers/sygus/sygus_grammar_cons.cpp  |   2 +-
 src/theory/quantifiers/term_util.cpp          |  12 +-
 .../preprocessing/pass_bv_gauss_white.cpp     | 262 +++++++++---------
 test/unit/theory/theory_bv_white.cpp          |   2 +-
 ...eory_quantifiers_bv_instantiator_white.cpp |  18 +-
 .../theory_quantifiers_bv_inverter_white.cpp  |  32 +--
 50 files changed, 380 insertions(+), 371 deletions(-)

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index d59733d76..8768bd996 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -96,7 +96,7 @@ int main()
 
   // Encoding code (2)
   // new_x_ = a + b - x
-  Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b);
+  Term a_plus_b = slv.mkTerm(BITVECTOR_ADD, a, b);
   Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x);
   Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x);
 
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 1ef0ea23f..6d97b93fa 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -94,7 +94,7 @@ public class BitVectors {
 
     // Encoding code (2)
     // new_x_ = a + b - x
-    Expr a_plus_b = em.mkExpr(Kind.BITVECTOR_PLUS, a, b);
+    Expr a_plus_b = em.mkExpr(Kind.BITVECTOR_ADD, a, b);
     Expr a_plus_b_minus_x = em.mkExpr(Kind.BITVECTOR_SUB, a_plus_b, x);
     Expr assignment2 = em.mkExpr(Kind.EQUAL, new_x_, a_plus_b_minus_x);
 
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index 1ddb02d8e..ff99bd785 100644
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -92,7 +92,7 @@ if __name__ == "__main__":
 
     # Encoding code (2)
     # new_x_ = a + b - x
-    a_plus_b = slv.mkTerm(kinds.BVPlus, a, b)
+    a_plus_b = slv.mkTerm(kinds.BVAdd, a, b)
     a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x)
     assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x)
 
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index ed35659f0..b7923321c 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -163,7 +163,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {BITVECTOR_XNOR, cvc5::Kind::BITVECTOR_XNOR},
     {BITVECTOR_COMP, cvc5::Kind::BITVECTOR_COMP},
     {BITVECTOR_MULT, cvc5::Kind::BITVECTOR_MULT},
-    {BITVECTOR_PLUS, cvc5::Kind::BITVECTOR_PLUS},
+    {BITVECTOR_ADD, cvc5::Kind::BITVECTOR_ADD},
     {BITVECTOR_SUB, cvc5::Kind::BITVECTOR_SUB},
     {BITVECTOR_NEG, cvc5::Kind::BITVECTOR_NEG},
     {BITVECTOR_UDIV, cvc5::Kind::BITVECTOR_UDIV},
@@ -442,7 +442,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR},
         {cvc5::Kind::BITVECTOR_COMP, BITVECTOR_COMP},
         {cvc5::Kind::BITVECTOR_MULT, BITVECTOR_MULT},
-        {cvc5::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS},
+        {cvc5::Kind::BITVECTOR_ADD, BITVECTOR_ADD},
         {cvc5::Kind::BITVECTOR_SUB, BITVECTOR_SUB},
         {cvc5::Kind::BITVECTOR_NEG, BITVECTOR_NEG},
         {cvc5::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV},
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index cad029b72..2805f6203 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -27,7 +27,9 @@ namespace api {
 /* Kind                                                                       */
 /* -------------------------------------------------------------------------- */
 
-// TODO(Gereon): Fix links that involve std::vector. See https://github.com/doxygen/doxygen/issues/8503
+// TODO(Gereon): Fix links that involve std::vector. See
+// https://github.com/doxygen/doxygen/issues/8503
+// clang-format off
 /**
  * The kind of a cvc5 term.
  *
@@ -888,7 +890,7 @@ enum CVC5_EXPORT Kind : int32_t
    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
-  BITVECTOR_PLUS,
+  BITVECTOR_ADD,
   /**
    * Subtraction of two bit-vectors.
    *
@@ -3389,6 +3391,7 @@ enum CVC5_EXPORT Kind : int32_t
   /** Marks the upper-bound of this enumeration. */
   LAST_KIND
 };
+// clang-format on
 
 /**
  * Get the string representation of a given kind.
diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py
index f0ac415e1..0c39bca6f 100644
--- a/src/api/parsekinds.py
+++ b/src/api/parsekinds.py
@@ -102,7 +102,7 @@ class KindsParser:
            so that the word after "Is" is capitalized
 
         Examples:
-           BITVECTOR_PLUS      -->  BVPlus
+           BITVECTOR_ADD       -->  BVAdd
            APPLY_SELECTOR      -->  ApplySelector
            FLOATINGPOINT_ISNAN -->  FPIsNan
            SETMINUS            -->  Setminus
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 02323b606..c2a6a30f6 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -140,7 +140,7 @@ const char* toString(PfRule id)
     case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR";
     case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP";
     case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT";
-    case PfRule::BV_BITBLAST_PLUS: return "BV_BITBLAST_PLUS";
+    case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD";
     case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB";
     case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG";
     case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index cfab15614..e4c33a840 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -757,7 +757,7 @@ enum class PfRule : uint32_t
   BV_BITBLAST_NOR,
   BV_BITBLAST_COMP,
   BV_BITBLAST_MULT,
-  BV_BITBLAST_PLUS,
+  BV_BITBLAST_ADD,
   BV_BITBLAST_SUB,
   BV_BITBLAST_NEG,
   BV_BITBLAST_UDIV,
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 6e3332651..c0a42ac26 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1904,7 +1904,7 @@ bvTerm[cvc5::api::Term& f]
       for (unsigned i = 0; i < args.size(); ++ i) {
         ENSURE_BV_SIZE(k, args[i]);
       }
-      f = MK_TERM(cvc5::api::BITVECTOR_PLUS, args);
+      f = MK_TERM(cvc5::api::BITVECTOR_ADD, args);
     }
     /* BV subtraction */
   | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c22b95af2..f3fd5697d 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -87,7 +87,7 @@ void Smt2::addBitvectorOperators() {
   addOperator(api::BITVECTOR_AND, "bvand");
   addOperator(api::BITVECTOR_OR, "bvor");
   addOperator(api::BITVECTOR_NEG, "bvneg");
-  addOperator(api::BITVECTOR_PLUS, "bvadd");
+  addOperator(api::BITVECTOR_ADD, "bvadd");
   addOperator(api::BITVECTOR_MULT, "bvmul");
   addOperator(api::BITVECTOR_UDIV, "bvudiv");
   addOperator(api::BITVECTOR_UREM, "bvurem");
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index f34ebd02e..b3c34087d 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -192,7 +192,7 @@ unsigned BVGauss::getMinBwExpr(Node expr)
           break;
         }
 
-        case kind::BITVECTOR_PLUS:
+        case kind::BITVECTOR_ADD:
         {
           Integer maxval = Integer(0);
           for (const Node& nn : n)
@@ -490,7 +490,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
 
       /* Split into matrix columns */
       Kind k = n.getKind();
-      if (k == kind::BITVECTOR_PLUS)
+      if (k == kind::BITVECTOR_ADD)
       {
         for (const Node& nn : n) { stack.push_back(nn); }
       }
@@ -668,16 +668,15 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
         }
         else
         {
-          Node tmp = stack.size() == 1
-                         ? stack[0]
-                         : nm->mkNode(kind::BITVECTOR_PLUS, stack);
+          Node tmp = stack.size() == 1 ? stack[0]
+                                       : nm->mkNode(kind::BITVECTOR_ADD, stack);
 
           if (rhs[prow] != 0)
           {
-            tmp = nm->mkNode(kind::BITVECTOR_PLUS,
-                             bv::utils::mkConst(
-                                 bv::utils::getSize(vvars[pcol]), rhs[prow]),
-                             tmp);
+            tmp = nm->mkNode(
+                kind::BITVECTOR_ADD,
+                bv::utils::mkConst(bv::utils::getSize(vvars[pcol]), rhs[prow]),
+                tmp);
           }
           Assert(!is_bv_const(tmp));
           res[vvars[pcol]] = nm->mkNode(kind::BITVECTOR_UREM, tmp, prime);
@@ -730,7 +729,7 @@ PreprocessingPassResult BVGauss::applyInternal(
         continue;
       }
 
-      if (urem[0].getKind() == kind::BITVECTOR_PLUS && is_bv_const(urem[1]))
+      if (urem[0].getKind() == kind::BITVECTOR_ADD && is_bv_const(urem[1]))
       {
         equations[urem[1]].push_back(a);
       }
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index c725081c2..8b5d2417b 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -100,7 +100,7 @@ Node BVToInt::makeBinary(Node n)
      */
     kind::Kind_t k = current.getKind();
     if ((numChildren > 2)
-        && (k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
+        && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT
             || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
             || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
     {
@@ -159,7 +159,7 @@ Node BVToInt::eliminationPass(Node n)
     CVC5_UNUSED kind::Kind_t k = current.getKind();
     uint64_t numChildren = current.getNumChildren();
     Assert((numChildren == 2)
-           || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
+           || !(k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT
                 || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
                 || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT));
     toVisit.pop_back();
@@ -347,7 +347,7 @@ Node BVToInt::translateWithChildren(Node original,
   Node returnNode;
   switch (oldKind)
   {
-    case kind::BITVECTOR_PLUS:
+    case kind::BITVECTOR_ADD:
     {
       Assert(originalNumChildren == 2);
       uint64_t bvsize = original[0].getType().getBitVectorSize();
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 2f9fd28e6..779e0a931 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -140,7 +140,7 @@ Node intToBV(TNode n, NodeMap& cache)
         {
           case kind::PLUS:
             Assert(children.size() == 2);
-            newKind = kind::BITVECTOR_PLUS;
+            newKind = kind::BITVECTOR_ADD;
             max = max + 1;
             break;
           case kind::MULT:
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 0d4804310..54115bb54 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -454,7 +454,7 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::XOR:
         case kind::BITVECTOR_XOR:
         case kind::BITVECTOR_XNOR:
-        case kind::BITVECTOR_PLUS:
+        case kind::BITVECTOR_ADD:
         case kind::BITVECTOR_SUB: checkParent = true; break;
 
         // Multiplication/division: must be non-integer and other operand must
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 8f433256d..42dfea308 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -702,8 +702,9 @@ void CvcPrinter::toStreamNode(std::ostream& out,
       op << "@";
       opType = INFIX;
       break;
-    case kind::BITVECTOR_PLUS: {
-      // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
+    case kind::BITVECTOR_ADD:
+    {
+      // This interprets a BITVECTOR_ADD as a bvadd in SMT-LIB
       Assert(n.getType().isBitVector());
       unsigned numc = n.getNumChildren()-2;
       unsigned child = 0;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 72d7fca89..2b1f16931 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -753,7 +753,10 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::BITVECTOR_XNOR: out << "bvxnor "; break;
   case kind::BITVECTOR_COMP: out << "bvcomp "; break;
   case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break;
-  case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break;
+  case kind::BITVECTOR_ADD:
+    out << "bvadd ";
+    forceBinary = true;
+    break;
   case kind::BITVECTOR_SUB: out << "bvsub "; break;
   case kind::BITVECTOR_NEG: out << "bvneg "; break;
   case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
@@ -1157,7 +1160,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::BITVECTOR_XNOR: return "bvxnor";
   case kind::BITVECTOR_COMP: return "bvcomp";
   case kind::BITVECTOR_MULT: return "bvmul";
-  case kind::BITVECTOR_PLUS: return "bvadd";
+  case kind::BITVECTOR_ADD: return "bvadd";
   case kind::BITVECTOR_SUB: return "bvsub";
   case kind::BITVECTOR_NEG: return "bvneg";
   case kind::BITVECTOR_UDIV: return "bvudiv";
diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp
index a5ab4a074..4fe1180be 100644
--- a/src/smt_util/nary_builder.cpp
+++ b/src/smt_util/nary_builder.cpp
@@ -129,7 +129,7 @@ bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
   case BITVECTOR_OR:
   case BITVECTOR_XOR:
   case BITVECTOR_MULT:
-  case BITVECTOR_PLUS:
+  case BITVECTOR_ADD:
   case DISTINCT:
   case PLUS:
   case MULT:
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index bb895fff2..f5259dc93 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -394,9 +394,11 @@ void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
 }
 
 template <class T>
-void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0);
+void DefaultAddBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
+{
+  Debug("bitvector-bb") << "theory::bv::DefaultAddBB bitblasting " << node
+                        << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_ADD && res.size() == 0);
 
   bb->bbTerm(node[0], res);
 
@@ -413,7 +415,6 @@ void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
   Assert(res.size() == utils::getSize(node));
 }
 
-
 template <class T>
 void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index a669e4a86..6e9444ba6 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -156,7 +156,7 @@ void TBitblaster<T>::initTermBBStrategies()
   d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
   d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
   d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
-  d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ADD] = DefaultAddBB<T>;
   d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
   d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
   d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index 4d6501673..6082a7128 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -46,7 +46,7 @@ std::unordered_map<Kind, PfRule, kind::KindHashFunction>
         {kind::BITVECTOR_NOR, PfRule::BV_BITBLAST_NOR},
         {kind::BITVECTOR_COMP, PfRule::BV_BITBLAST_COMP},
         {kind::BITVECTOR_MULT, PfRule::BV_BITBLAST_MULT},
-        {kind::BITVECTOR_PLUS, PfRule::BV_BITBLAST_PLUS},
+        {kind::BITVECTOR_ADD, PfRule::BV_BITBLAST_ADD},
         {kind::BITVECTOR_SUB, PfRule::BV_BITBLAST_SUB},
         {kind::BITVECTOR_NEG, PfRule::BV_BITBLAST_NEG},
         {kind::BITVECTOR_UDIV, PfRule::BV_BITBLAST_UDIV},
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 06ecea701..fbd910bee 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -434,15 +434,15 @@ TrustNode BVSolverLazy::ppRewrite(TNode t)
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
     res = Rewriter::rewrite(result);
   }
-  else if (RewriteRule<UltPlusOne>::applies(t))
+  else if (RewriteRule<UltAddOne>::applies(t))
   {
-    Node result = RewriteRule<UltPlusOne>::run<false>(t);
+    Node result = RewriteRule<UltAddOne>::run<false>(t);
     res = Rewriter::rewrite(result);
   }
   else if (res.getKind() == kind::EQUAL
-           && ((res[0].getKind() == kind::BITVECTOR_PLUS
+           && ((res[0].getKind() == kind::BITVECTOR_ADD
                 && RewriteRule<ConcatToMult>::applies(res[1]))
-               || (res[1].getKind() == kind::BITVECTOR_PLUS
+               || (res[1].getKind() == kind::BITVECTOR_ADD
                    && RewriteRule<ConcatToMult>::applies(res[0]))))
   {
     Node mult = RewriteRule<ConcatToMult>::applies(res[0])
@@ -469,20 +469,20 @@ TrustNode BVSolverLazy::ppRewrite(TNode t)
   {
     res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
   }
-  else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
+  else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
   {
-    res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
+    res = RewriteRule<NormalizeEqAddNeg>::run<false>(t);
   }
 
   // if(t.getKind() == kind::EQUAL &&
   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
-  //    kind::BITVECTOR_PLUS) ||
+  //    kind::BITVECTOR_ADD) ||
   //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
-  //     kind::BITVECTOR_PLUS))) {
+  //     kind::BITVECTOR_ADD))) {
   //   // if we have an equality between a multiplication and addition
   //   // try to express multiplication in terms of addition
   //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
-  //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
+  //   Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1];
   //   if (RewriteRule<MultSlice>::applies(mult)) {
   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
   //     Node new_eq =
@@ -653,13 +653,13 @@ void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned)
 
   if (in.getKind() == kind::EQUAL)
   {
-    if ((in[0].getKind() == kind::BITVECTOR_PLUS
+    if ((in[0].getKind() == kind::BITVECTOR_ADD
          && in[1].getKind() == kind::BITVECTOR_SHL)
-        || (in[1].getKind() == kind::BITVECTOR_PLUS
+        || (in[1].getKind() == kind::BITVECTOR_ADD
             && in[0].getKind() == kind::BITVECTOR_SHL))
     {
-      TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
-      TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
+      TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
+      TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];
 
       if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
           && p[1].getKind() == kind::BITVECTOR_SHL)
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 7f3099f8c..7c97d1bbc 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -136,7 +136,7 @@ void CoreSolver::finishInit()
   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
   d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true);
-  d_equalityEngine->addFunctionKind(kind::BITVECTOR_PLUS, true);
+  d_equalityEngine->addFunctionKind(kind::BITVECTOR_ADD, true);
   d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
   //    d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 10b9a346e..aa93008c2 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -237,7 +237,7 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
 
   Node one = utils::mkConst(utils::getSize(a), 1);
   Node a_plus_one = Rewriter::rewrite(
-      NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, a, one));
+      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, a, one));
   if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end())
   {
     ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact);
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index c9999d39b..6af586735 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -57,7 +57,7 @@ operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors"
 ## arithmetic kinds
 operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
 operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
-operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
+operator BITVECTOR_ADD 2: "addition of two or more bit-vectors"
 operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
 operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
 operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
@@ -179,7 +179,7 @@ typerule BITVECTOR_XOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 ## arithmetic kinds
 typerule BITVECTOR_MULT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_NEG ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_PLUS ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ADD ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SUB ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_UDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_UREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp
index b8ede6386..93ba9e67f 100644
--- a/src/theory/bv/proof_checker.cpp
+++ b/src/theory/bv/proof_checker.cpp
@@ -43,7 +43,7 @@ void BVProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::BV_BITBLAST_NOR, this);
   pc->registerChecker(PfRule::BV_BITBLAST_COMP, this);
   pc->registerChecker(PfRule::BV_BITBLAST_MULT, this);
-  pc->registerChecker(PfRule::BV_BITBLAST_PLUS, this);
+  pc->registerChecker(PfRule::BV_BITBLAST_ADD, this);
   pc->registerChecker(PfRule::BV_BITBLAST_SUB, this);
   pc->registerChecker(PfRule::BV_BITBLAST_NEG, this);
   pc->registerChecker(PfRule::BV_BITBLAST_UDIV, this);
@@ -89,7 +89,7 @@ Node BVProofRuleChecker::checkInternal(PfRule id,
            || id == PfRule::BV_BITBLAST_OR || id == PfRule::BV_BITBLAST_XOR
            || id == PfRule::BV_BITBLAST_XNOR || id == PfRule::BV_BITBLAST_NAND
            || id == PfRule::BV_BITBLAST_NOR || id == PfRule::BV_BITBLAST_COMP
-           || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_PLUS
+           || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_ADD
            || id == PfRule::BV_BITBLAST_SUB || id == PfRule::BV_BITBLAST_NEG
            || id == PfRule::BV_BITBLAST_UDIV || id == PfRule::BV_BITBLAST_UREM
            || id == PfRule::BV_BITBLAST_SDIV || id == PfRule::BV_BITBLAST_SREM
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 296fca2c0..c5ab08f0c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -112,7 +112,7 @@ void TheoryBV::finishInit()
     //    ee->addFunctionKind(kind::BITVECTOR_XNOR);
     //    ee->addFunctionKind(kind::BITVECTOR_COMP);
     ee->addFunctionKind(kind::BITVECTOR_MULT, true);
-    ee->addFunctionKind(kind::BITVECTOR_PLUS, true);
+    ee->addFunctionKind(kind::BITVECTOR_ADD, true);
     ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
     //    ee->addFunctionKind(kind::BITVECTOR_SUB);
     //    ee->addFunctionKind(kind::BITVECTOR_NEG);
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 7fe9559f9..040d2c53f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -89,7 +89,7 @@ enum RewriteRuleId
   EvalXor,
   EvalNot,
   EvalMult,
-  EvalPlus,
+  EvalAdd,
   EvalUdiv,
   EvalUrem,
   EvalShl,
@@ -181,14 +181,14 @@ enum RewriteRuleId
   DoubleNeg,
   NegMult,
   NegSub,
-  NegPlus,
+  NegAdd,
   NotConcat,
   NotAnd,  // not sure why this would help (not done)
   NotOr,   // not sure why this would help (not done)
   NotXor,  // not sure why this would help (not done)
   FlattenAssocCommut,
   FlattenAssocCommutNoDuplicates,
-  PlusCombineLikeTerms,
+  AddCombineLikeTerms,
   MultSimplify,
   MultDistribConst,
   MultDistrib,
@@ -198,10 +198,10 @@ enum RewriteRuleId
   OrSimplify,
   XorSimplify,
   BitwiseSlicing,
-  NormalizeEqPlusNeg,
+  NormalizeEqAddNeg,
   // rules to simplify bitblasting
-  BBPlusNeg,
-  UltPlusOne,
+  BBAddNeg,
+  UltAddOne,
   ConcatToMult,
   IsPowerOfTwo,
   MultSltMult,
@@ -258,7 +258,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case EvalXor :            out << "EvalXor";             return out;
   case EvalNot :            out << "EvalNot";             return out;
   case EvalMult :           out << "EvalMult";            return out;
-  case EvalPlus :           out << "EvalPlus";            return out;
+  case EvalAdd: out << "EvalAdd"; return out;
   case EvalUdiv :           out << "EvalUdiv";            return out;
   case EvalUrem :           out << "EvalUrem";            return out;
   case EvalShl :            out << "EvalShl";             return out;
@@ -340,8 +340,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case NotIdemp :                  out << "NotIdemp"; return out;
   case UleSelf:                    out << "UleSelf"; return out; 
   case FlattenAssocCommut:     out << "FlattenAssocCommut"; return out;
-  case FlattenAssocCommutNoDuplicates:     out << "FlattenAssocCommutNoDuplicates"; return out; 
-  case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out;
+  case FlattenAssocCommutNoDuplicates:
+    out << "FlattenAssocCommutNoDuplicates";
+    return out;
+  case AddCombineLikeTerms: out << "AddCombineLikeTerms"; return out;
   case MultSimplify: out << "MultSimplify"; return out;
   case MultDistribConst: out << "MultDistribConst"; return out;
   case SolveEq : out << "SolveEq"; return out;
@@ -351,8 +353,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case AndSimplify : out << "AndSimplify"; return out;
   case OrSimplify : out << "OrSimplify"; return out;
   case XorSimplify : out << "XorSimplify"; return out;
-  case NegPlus : out << "NegPlus"; return out;
-  case BBPlusNeg : out << "BBPlusNeg"; return out;
+  case NegAdd: out << "NegAdd"; return out;
+  case BBAddNeg: out << "BBAddNeg"; return out;
   case UltOne : out << "UltOne"; return out;
   case SltZero : out << "SltZero"; return out;
   case ZeroUlt : out << "ZeroUlt"; return out;
@@ -366,11 +368,11 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case BitwiseSlicing : out << "BitwiseSlicing"; return out;
   case ExtractSignExtend : out << "ExtractSignExtend"; return out;
   case MultDistrib: out << "MultDistrib"; return out;
-  case UltPlusOne: out << "UltPlusOne"; return out;
+  case UltAddOne: out << "UltAddOne"; return out;
   case ConcatToMult: out << "ConcatToMult"; return out;
   case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
   case MultSltMult: out << "MultSltMult"; return out;
-  case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out;
+  case NormalizeEqAddNeg: out << "NormalizeEqAddNeg"; return out;
   case BitOfConst: out << "BitOfConst"; return out;
   default:
     Unreachable();
@@ -513,7 +515,7 @@ struct AllRewriteRules {
   RewriteRule<EvalNot>                        rule29;
   RewriteRule<EvalSlt>                        rule30;
   RewriteRule<EvalMult>                       rule31;
-  RewriteRule<EvalPlus>                       rule32;
+  RewriteRule<EvalAdd> rule32;
   RewriteRule<XorSimplify>                    rule33;
   RewriteRule<EvalUdiv>                       rule34;
   RewriteRule<EvalUrem>                       rule35;
@@ -582,13 +584,13 @@ struct AllRewriteRules {
   RewriteRule<NotIdemp>                       rule102;
   RewriteRule<UleSelf>                        rule103;
   RewriteRule<FlattenAssocCommut>             rule104;
-  RewriteRule<PlusCombineLikeTerms>           rule105;
+  RewriteRule<AddCombineLikeTerms> rule105;
   RewriteRule<MultSimplify>                   rule106;
   RewriteRule<MultDistribConst>               rule107;
   RewriteRule<AndSimplify>                    rule108;
   RewriteRule<OrSimplify>                     rule109;
-  RewriteRule<NegPlus>                        rule110;
-  RewriteRule<BBPlusNeg>                      rule111;
+  RewriteRule<NegAdd> rule110;
+  RewriteRule<BBAddNeg> rule111;
   RewriteRule<SolveEq>                        rule112;
   RewriteRule<BitwiseEq>                      rule113;
   RewriteRule<UltOne>                         rule114;
@@ -596,7 +598,7 @@ struct AllRewriteRules {
   RewriteRule<BVToNatEliminate>               rule116;
   RewriteRule<IntToBVEliminate>               rule117;
   RewriteRule<MultDistrib>                    rule118;
-  RewriteRule<UltPlusOne>                     rule119;
+  RewriteRule<UltAddOne> rule119;
   RewriteRule<ConcatToMult>                   rule120;
   RewriteRule<IsPowerOfTwo>                   rule121;
   RewriteRule<RedorEliminate>                 rule122;
@@ -606,7 +608,7 @@ struct AllRewriteRules {
   RewriteRule<SignExtendUltConst>             rule126;
   RewriteRule<ZeroExtendUltConst>             rule127;
   RewriteRule<MultSltMult>                    rule128;
-  RewriteRule<NormalizeEqPlusNeg>             rule129;
+  RewriteRule<NormalizeEqAddNeg> rule129;
   RewriteRule<BvComp>                         rule130;
   RewriteRule<BvIteConstCond>                 rule131;
   RewriteRule<BvIteEqualChildren>             rule132;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 1c229ed72..af80ad00b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -151,15 +151,16 @@ Node RewriteRule<EvalMult>::apply(TNode node) {
   return utils::mkConst(res);
 }
 
-template<> inline
-bool RewriteRule<EvalPlus>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_PLUS &&
-          utils::isBvConstTerm(node));
+template <>
+inline bool RewriteRule<EvalAdd>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ADD && utils::isBvConstTerm(node));
 }
 
-template<> inline
-Node RewriteRule<EvalPlus>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
+template <>
+inline Node RewriteRule<EvalAdd>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<EvalAdd>(" << node << ")" << std::endl;
   TNode::iterator child_it = node.begin();
   BitVector res = (*child_it).getConst<BitVector>();
   for(++child_it; child_it != node.end(); ++child_it) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 4a2d2943d..45e313e48 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -146,10 +146,10 @@ inline Node RewriteRule<ExtractSignExtend>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<ExtractArith>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
-          utils::getExtractLow(node) == 0 &&
-          (node[0].getKind() == kind::BITVECTOR_PLUS ||
-           node[0].getKind() == kind::BITVECTOR_MULT));
+  return (node.getKind() == kind::BITVECTOR_EXTRACT
+          && utils::getExtractLow(node) == 0
+          && (node[0].getKind() == kind::BITVECTOR_ADD
+              || node[0].getKind() == kind::BITVECTOR_MULT));
 }
 
 template <>
@@ -178,9 +178,9 @@ inline Node RewriteRule<ExtractArith>::apply(TNode node)
 // careful not to apply in a loop 
 template<> inline
 bool RewriteRule<ExtractArith2>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
-          (node[0].getKind() == kind::BITVECTOR_PLUS ||
-           node[0].getKind() == kind::BITVECTOR_MULT));
+  return (node.getKind() == kind::BITVECTOR_EXTRACT
+          && (node[0].getKind() == kind::BITVECTOR_ADD
+              || node[0].getKind() == kind::BITVECTOR_MULT));
 }
 
 template <>
@@ -204,11 +204,9 @@ inline Node RewriteRule<ExtractArith2>::apply(TNode node)
 template<> inline
 bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
   Kind kind = node.getKind();
-  if (kind != kind::BITVECTOR_PLUS &&
-      kind != kind::BITVECTOR_MULT &&
-      kind != kind::BITVECTOR_OR &&
-      kind != kind::BITVECTOR_XOR &&
-      kind != kind::BITVECTOR_AND)
+  if (kind != kind::BITVECTOR_ADD && kind != kind::BITVECTOR_MULT
+      && kind != kind::BITVECTOR_OR && kind != kind::BITVECTOR_XOR
+      && kind != kind::BITVECTOR_AND)
     return false;
   TNode::iterator child_it = node.begin();
   for(; child_it != node.end(); ++child_it) {
@@ -247,7 +245,7 @@ inline Node RewriteRule<FlattenAssocCommut>::apply(TNode node)
       children.push_back(current);
     }
   }
-  if (node.getKind() == kind::BITVECTOR_PLUS
+  if (node.getKind() == kind::BITVECTOR_ADD
       || node.getKind() == kind::BITVECTOR_MULT)
   {
     return utils::mkNaryNode(kind, children);
@@ -371,15 +369,16 @@ static inline void addToChildren(TNode term,
   }
 }
 
-template<> inline
-bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_PLUS);
+template <>
+inline bool RewriteRule<AddCombineLikeTerms>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_ADD);
 }
 
 template <>
-inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node)
+inline Node RewriteRule<AddCombineLikeTerms>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")"
+  Debug("bv-rewrite") << "RewriteRule<AddCombineLikeTerms>(" << node << ")"
                       << std::endl;
   unsigned size = utils::getSize(node);
   BitVector constSum(size, (unsigned)0);
@@ -419,9 +418,8 @@ inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node)
     return node;
   }
 
-  return csize == 0
-    ? utils::mkZero(size)
-    : utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
+  return csize == 0 ? utils::mkZero(size)
+                    : utils::mkNaryNode(kind::BITVECTOR_ADD, children);
 }
 
 template<> inline
@@ -508,9 +506,9 @@ bool RewriteRule<MultDistribConst>::applies(TNode node) {
     return false;
   }
   TNode factor = node[0];
-  return (factor.getKind() == kind::BITVECTOR_PLUS ||
-          factor.getKind() == kind::BITVECTOR_SUB ||
-          factor.getKind() == kind::BITVECTOR_NEG); 
+  return (factor.getKind() == kind::BITVECTOR_ADD
+          || factor.getKind() == kind::BITVECTOR_SUB
+          || factor.getKind() == kind::BITVECTOR_NEG);
 }
 
 template <>
@@ -547,13 +545,14 @@ bool RewriteRule<MultDistrib>::applies(TNode node) {
       node.getNumChildren() != 2) {
     return false;
   }
-  if (node[0].getKind() == kind::BITVECTOR_PLUS ||
-      node[0].getKind() == kind::BITVECTOR_SUB) {
-    return node[1].getKind() != kind::BITVECTOR_PLUS &&
-           node[1].getKind() != kind::BITVECTOR_SUB;
+  if (node[0].getKind() == kind::BITVECTOR_ADD
+      || node[0].getKind() == kind::BITVECTOR_SUB)
+  {
+    return node[1].getKind() != kind::BITVECTOR_ADD
+           && node[1].getKind() != kind::BITVECTOR_SUB;
   }
-  return node[1].getKind() == kind::BITVECTOR_PLUS ||
-         node[1].getKind() == kind::BITVECTOR_SUB; 
+  return node[1].getKind() == kind::BITVECTOR_ADD
+         || node[1].getKind() == kind::BITVECTOR_SUB;
 }
 
 template <>
@@ -563,13 +562,13 @@ inline Node RewriteRule<MultDistrib>::apply(TNode node)
                       << std::endl;
 
   NodeManager *nm = NodeManager::currentNM();
-  bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS
+  bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_ADD
                        || node[0].getKind() == kind::BITVECTOR_SUB;
   TNode factor = !is_rhs_factor ? node[0] : node[1];
   TNode sum = is_rhs_factor ? node[0] : node[1];
-  Assert(factor.getKind() != kind::BITVECTOR_PLUS
+  Assert(factor.getKind() != kind::BITVECTOR_ADD
          && factor.getKind() != kind::BITVECTOR_SUB
-         && (sum.getKind() == kind::BITVECTOR_PLUS
+         && (sum.getKind() == kind::BITVECTOR_ADD
              || sum.getKind() == kind::BITVECTOR_SUB));
 
   std::vector<Node> children;
@@ -643,7 +642,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node)
   std::map<Node, BitVector> leftMap, rightMap;
 
   // Collect terms and coefficients plus constant for left
-  if (left.getKind() == kind::BITVECTOR_PLUS)
+  if (left.getKind() == kind::BITVECTOR_ADD)
   {
     for (unsigned i = 0; i < left.getNumChildren(); ++i)
     {
@@ -660,7 +659,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node)
   }
 
   // Collect terms and coefficients plus constant for right
-  if (right.getKind() == kind::BITVECTOR_PLUS)
+  if (right.getKind() == kind::BITVECTOR_ADD)
   {
     for (unsigned i = 0; i < right.getNumChildren(); ++i)
     {
@@ -819,7 +818,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node)
   }
   else
   {
-    newLeft = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenLeft);
+    newLeft = utils::mkNaryNode(kind::BITVECTOR_ADD, childrenLeft);
   }
 
   if (childrenRight.size() == 0)
@@ -828,7 +827,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node)
   }
   else
   {
-    newRight = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenRight);
+    newRight = utils::mkNaryNode(kind::BITVECTOR_ADD, childrenRight);
   }
 
   if (!changed)
@@ -1018,23 +1017,24 @@ inline Node RewriteRule<NegSub>::apply(TNode node)
       kind::BITVECTOR_SUB, node[0][1], node[0][0]);
 }
 
-template<> inline
-bool RewriteRule<NegPlus>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_NEG &&
-          node[0].getKind() == kind::BITVECTOR_PLUS);
+template <>
+inline bool RewriteRule<NegAdd>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_NEG
+          && node[0].getKind() == kind::BITVECTOR_ADD);
 }
 
 template <>
-inline Node RewriteRule<NegPlus>::apply(TNode node)
+inline Node RewriteRule<NegAdd>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NegAdd>(" << node << ")" << std::endl;
   NodeManager *nm = NodeManager::currentNM();
   std::vector<Node> children;
   for (unsigned i = 0; i < node[0].getNumChildren(); ++i)
   {
     children.push_back(nm->mkNode(kind::BITVECTOR_NEG, node[0][i]));
   }
-  return utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
+  return utils::mkNaryNode(kind::BITVECTOR_ADD, children);
 }
 
 struct Count {
@@ -1480,24 +1480,24 @@ inline Node RewriteRule<BitwiseSlicing>::apply(TNode node)
 }
 
 template <>
-inline bool RewriteRule<NormalizeEqPlusNeg>::applies(TNode node)
+inline bool RewriteRule<NormalizeEqAddNeg>::applies(TNode node)
 {
   return node.getKind() == kind::EQUAL
-         && (node[0].getKind() == kind::BITVECTOR_PLUS
-             || node[1].getKind() == kind::BITVECTOR_PLUS);
+         && (node[0].getKind() == kind::BITVECTOR_ADD
+             || node[1].getKind() == kind::BITVECTOR_ADD);
 }
 
 template <>
-inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
+inline Node RewriteRule<NormalizeEqAddNeg>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")"
+  Debug("bv-rewrite") << "RewriteRule<NormalizeEqAddNeg>(" << node << ")"
                       << std::endl;
 
-  NodeBuilder nb_lhs(kind::BITVECTOR_PLUS);
-  NodeBuilder nb_rhs(kind::BITVECTOR_PLUS);
+  NodeBuilder nb_lhs(kind::BITVECTOR_ADD);
+  NodeBuilder nb_rhs(kind::BITVECTOR_ADD);
   NodeManager *nm = NodeManager::currentNM();
 
-  if (node[0].getKind() == kind::BITVECTOR_PLUS)
+  if (node[0].getKind() == kind::BITVECTOR_ADD)
   {
     for (const TNode &n : node[0])
     {
@@ -1512,7 +1512,7 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
     nb_lhs << node[0];
   }
 
-  if (node[1].getKind() == kind::BITVECTOR_PLUS)
+  if (node[1].getKind() == kind::BITVECTOR_ADD)
   {
     for (const TNode &n : node[1])
     {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 023bbf55c..e44d1c9b7 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -50,8 +50,7 @@ inline Node RewriteRule<NegEliminate>::apply(TNode node)
   unsigned size = utils::getSize(a);
   Node one = utils::mkOne(size);
   Node nota = nm->mkNode(kind::BITVECTOR_NOT, a);
-  Node bvadd =
-      nm->mkNode(kind::BITVECTOR_PLUS, nota, one);
+  Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, nota, one);
   return bvadd;
 }
 
@@ -75,7 +74,7 @@ inline Node RewriteRule<OrEliminate>::apply(TNode node)
   NodeManager* nm = NodeManager::currentNM();
   TNode a = node[0];
   TNode b = node[1];
-  Node bvadd = nm->mkNode(kind::BITVECTOR_PLUS, a, b);
+  Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, a, b);
   Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b);
   Node result =
       nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand);
@@ -191,8 +190,8 @@ inline Node RewriteRule<SltEliminate>::apply(TNode node)
   unsigned size = utils::getSize(node[0]);
   Integer val = Integer(1).multiplyByPow2(size - 1);
   Node pow_two = utils::mkConst(size, val);
-  Node a = nm->mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
-  Node b = nm->mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
+  Node a = nm->mkNode(kind::BITVECTOR_ADD, node[0], pow_two);
+  Node b = nm->mkNode(kind::BITVECTOR_ADD, node[1], pow_two);
 
   return nm->mkNode(kind::BITVECTOR_ULT, a, b);
 }
@@ -267,7 +266,7 @@ inline Node RewriteRule<SubEliminate>::apply(TNode node)
   Node negb = nm->mkNode(kind::BITVECTOR_NEG, node[1]);
   Node a = node[0];
 
-  return nm->mkNode(kind::BITVECTOR_PLUS, a, negb);
+  return nm->mkNode(kind::BITVECTOR_ADD, a, negb);
 }
 
 template <>
@@ -636,8 +635,8 @@ inline Node RewriteRule<SmodEliminate>::apply(TNode node)
       cond1.iteNode(
           u,
           cond2.iteNode(
-              nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t),
-              cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u))));
+              nm->mkNode(kind::BITVECTOR_ADD, neg_u, t),
+              cond3.iteNode(nm->mkNode(kind::BITVECTOR_ADD, u, t), neg_u))));
 
   return result;
 }
@@ -703,8 +702,8 @@ inline Node RewriteRule<SmodEliminateFewerBitwiseOps>::apply(TNode node)
       cond1.iteNode(
           u,
           cond2.iteNode(
-              nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t),
-              cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u))));
+              nm->mkNode(kind::BITVECTOR_ADD, neg_u, t),
+              cond3.iteNode(nm->mkNode(kind::BITVECTOR_ADD, u, t), neg_u))));
 
   return result;
 }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 949dbce1a..1e38aba0f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1610,16 +1610,18 @@ inline Node RewriteRule<UgtUrem>::apply(TNode node)
 /* -------------------------------------------------------------------------- */
 
 /**
- * BBPlusNeg
- * 
+ * BBAddNeg
+ *
  * -a1 - a2 - ... - an + ak + ..  ==> - (a1 + a2 + ... + an) + ak
  *
  */
 
-template<> inline
-bool RewriteRule<BBPlusNeg>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_PLUS) {
-    return false; 
+template <>
+inline bool RewriteRule<BBAddNeg>::applies(TNode node)
+{
+  if (node.getKind() != kind::BITVECTOR_ADD)
+  {
+    return false;
   }
 
   unsigned neg_count = 0; 
@@ -1632,9 +1634,9 @@ bool RewriteRule<BBPlusNeg>::applies(TNode node) {
 }
 
 template <>
-inline Node RewriteRule<BBPlusNeg>::apply(TNode node)
+inline Node RewriteRule<BBAddNeg>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<BBAddNeg>(" << node << ")" << std::endl;
   NodeManager *nm = NodeManager::currentNM();
   std::vector<Node> children;
   unsigned neg_count = 0;
@@ -1653,7 +1655,7 @@ inline Node RewriteRule<BBPlusNeg>::apply(TNode node)
   Assert(neg_count != 0);
   children.push_back(utils::mkConst(utils::getSize(node), neg_count));
 
-  return utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
+  return utils::mkNaryNode(kind::BITVECTOR_ADD, children);
 }
 
 /* -------------------------------------------------------------------------- */
@@ -2003,7 +2005,7 @@ inline Node RewriteRule<MultSlice>::apply(TNode node)
   Node term3 = nm->mkNode(kind::BITVECTOR_CONCAT,
                           nm->mkNode(kind::BITVECTOR_MULT, top_a, bottom_b),
                           zeros);
-  return nm->mkNode(kind::BITVECTOR_PLUS, term1, term2, term3);
+  return nm->mkNode(kind::BITVECTOR_ADD, term1, term2, term3);
 }
 
 /* -------------------------------------------------------------------------- */
@@ -2015,12 +2017,13 @@ inline Node RewriteRule<MultSlice>::apply(TNode node)
  * 
  * @return 
  */
-template<> inline
-bool RewriteRule<UltPlusOne>::applies(TNode node) {
+template <>
+inline bool RewriteRule<UltAddOne>::applies(TNode node)
+{
   if (node.getKind() != kind::BITVECTOR_ULT) return false;
   TNode x = node[0];
   TNode y1 = node[1];
-  if (y1.getKind() != kind::BITVECTOR_PLUS) return false;
+  if (y1.getKind() != kind::BITVECTOR_ADD) return false;
   if (y1[0].getKind() != kind::CONST_BITVECTOR &&
       y1[1].getKind() != kind::CONST_BITVECTOR)
     return false;
@@ -2034,13 +2037,13 @@ bool RewriteRule<UltPlusOne>::applies(TNode node) {
 
   TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1];
   if (one != utils::mkConst(utils::getSize(one), 1)) return false;
-  return true; 
+  return true;
 }
 
 template <>
-inline Node RewriteRule<UltPlusOne>::apply(TNode node)
+inline Node RewriteRule<UltAddOne>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UltAddOne>(" << node << ")" << std::endl;
   NodeManager *nm = NodeManager::currentNM();
   TNode x = node[0];
   TNode y1 = node[1];
@@ -2188,12 +2191,12 @@ bool RewriteRule<MultSltMult>::applies(TNode node)
     return false;
 
   TNode addxt, x, a;
-  if (ml[0].getKind() == kind::BITVECTOR_PLUS)
+  if (ml[0].getKind() == kind::BITVECTOR_ADD)
   {
     addxt = ml[0];
     a = ml[1];
   }
-  else if (ml[1].getKind() == kind::BITVECTOR_PLUS)
+  else if (ml[1].getKind() == kind::BITVECTOR_ADD)
   {
     addxt = ml[1];
     a = ml[0];
@@ -2228,14 +2231,14 @@ Node RewriteRule<MultSltMult>::apply(TNode node)
   std::tie(mr[0], mr[1], std::ignore) = extract_ext_tuple(node[1]);
 
   TNode addxt, x, t, a;
-  if (ml[0].getKind() == kind::BITVECTOR_PLUS)
+  if (ml[0].getKind() == kind::BITVECTOR_ADD)
   {
     addxt = ml[0];
     a = ml[1];
   }
   else
   {
-    Assert(ml[1].getKind() == kind::BITVECTOR_PLUS);
+    Assert(ml[1].getKind() == kind::BITVECTOR_ADD);
     addxt = ml[1];
     a = ml[0];
   }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index bda212351..d0579703d 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -412,7 +412,8 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
+RewriteResponse TheoryBVRewriter::RewriteAdd(TNode node, bool prerewrite)
+{
   Node resultNode = node;
   if (prerewrite) {
     resultNode = LinearRewriteStrategy
@@ -420,17 +421,16 @@ RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
         >::apply(node);
     return RewriteResponse(REWRITE_DONE, resultNode);
   }
-  
-  resultNode =  LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<PlusCombineLikeTerms>
-      >::apply(node);
+
+  resultNode =
+      LinearRewriteStrategy<RewriteRule<FlattenAssocCommut>,
+                            RewriteRule<AddCombineLikeTerms>>::apply(node);
 
   if (node != resultNode) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
   }
-  
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+
+  return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
@@ -450,12 +450,13 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
       RewriteRule<NegIdemp>,
       RewriteRule<NegSub>
       >::apply(node);
-  
-  if (RewriteRule<NegPlus>::applies(node)) {
-    resultNode = RewriteRule<NegPlus>::run<false>(node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+
+  if (RewriteRule<NegAdd>::applies(node))
+  {
+    resultNode = RewriteRule<NegAdd>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
   }
-  
+
   if(!prerewrite) {
     if (RewriteRule<NegMult>::applies(node)) {
       resultNode = RewriteRule<NegMult>::run<false>(node);
@@ -718,7 +719,7 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_NOR ] = RewriteNor;
   d_rewriteTable [ kind::BITVECTOR_COMP ] = RewriteComp;
   d_rewriteTable [ kind::BITVECTOR_MULT ] = RewriteMult;
-  d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus;
+  d_rewriteTable[kind::BITVECTOR_ADD] = RewriteAdd;
   d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub;
   d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg;
   d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 56eb718df..9dc1ab351 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -76,7 +76,7 @@ class TheoryBVRewriter : public TheoryRewriter
   static RewriteResponse RewriteNor(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteComp(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteMult(TNode node, bool prerewrite = false);
-  static RewriteResponse RewritePlus(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteAdd(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSub(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 1549df639..927a40b82 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -398,7 +398,7 @@ Node mkConcat(TNode node, unsigned repeat)
 Node mkInc(TNode t)
 {
   return NodeManager::currentNM()->mkNode(
-      kind::BITVECTOR_PLUS, t, mkOne(getSize(t)));
+      kind::BITVECTOR_ADD, t, mkOne(getSize(t)));
 }
 
 Node mkDec(TNode t)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 8e916e975..fca449917 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -118,7 +118,7 @@ Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes)
 {
   Assert(k == kind::AND || k == kind::OR || k == kind::XOR
          || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
-         || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_PLUS
+         || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_ADD
          || k == kind::BITVECTOR_SUB || k == kind::BITVECTOR_MULT);
 
   if (nodes.size() == 1) { return nodes[0]; }
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index da6ff9803..36dfc710b 100644
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -336,11 +336,11 @@ bool SygusSimpleSymBreak::considerArgKind(
       //  (~ (- y z) x)  ---->  (~ y (+ x z))
       rt.d_req_kind = pk;
       rt.d_children[arg].d_req_type = dt[c].getArgType(0);
-      rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS;
+      rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_ADD;
       rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
       rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
     }
-    else if (pk == PLUS || pk == BITVECTOR_PLUS)
+    else if (pk == PLUS || pk == BITVECTOR_ADD)
     {
       //  (+ x (- y z))  -----> (- (+ x y) z)
       //  (+ (- y z) x)  -----> (- (+ x y) z)
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index c0a3a2a2f..07a4e4b85 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -734,7 +734,7 @@ EvalResult Evaluator::evalInternal(
           break;
         }
 
-        case kind::BITVECTOR_PLUS:
+        case kind::BITVECTOR_ADD:
         {
           BitVector res = results[currNode[0]].d_bv;
           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index a2306cc6a..3a058772c 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -477,7 +477,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+(
     const symbolicBitVector<isSigned> &op) const
 {
   return symbolicBitVector<isSigned>(
-      NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op));
+      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, *this, op));
 }
 
 template <bool isSigned>
@@ -530,7 +530,7 @@ template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::increment() const
 {
   return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
-      kind::BITVECTOR_PLUS, *this, one(this->getWidth())));
+      kind::BITVECTOR_ADD, *this, one(this->getWidth())));
 }
 
 template <bool isSigned>
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 86444b8cf..fd204fffd 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -108,7 +108,7 @@ static bool isInvertible(Kind k, unsigned index)
   return k == NOT || k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT
          || k == BITVECTOR_COMP || k == BITVECTOR_NOT || k == BITVECTOR_NEG
          || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND
-         || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_UREM
+         || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_UREM
          || k == BITVECTOR_UDIV || k == BITVECTOR_AND || k == BITVECTOR_OR
          || k == BITVECTOR_XOR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR
          || k == BITVECTOR_SHL;
@@ -284,7 +284,7 @@ Node BvInverter::solveBvLit(Node sv,
     {
       t = nm->mkNode(k, t);
     }
-    else if (litk == EQUAL && k == BITVECTOR_PLUS)
+    else if (litk == EQUAL && k == BITVECTOR_ADD)
     {
       t = nm->mkNode(BITVECTOR_SUB, t, s);
     }
diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp
index ff932cf15..e7427178a 100644
--- a/src/theory/quantifiers/bv_inverter_utils.cpp
+++ b/src/theory/quantifiers/bv_inverter_utils.cpp
@@ -327,7 +327,7 @@ Node getICBvUrem(
          *          (or (= t z) (distinct (bvsub s (_ bv1 w)) t))))
          * where
          * z = 0 with getSize(z) = w  */
-        Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
+        Node add = nm->mkNode(BITVECTOR_ADD, t, t);
         Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
         Node a = nm->mkNode(BITVECTOR_AND, sub, s);
         scl = nm->mkNode(BITVECTOR_UGE, a, t);
@@ -386,7 +386,7 @@ Node getICBvUrem(
          * (or
          *   (bvuge (bvand (bvsub (bvadd t t) s) s) t)  ; eq, synthesized
          *   (bvult t s))                               ; ugt, synthesized  */
-        Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
+        Node add = nm->mkNode(BITVECTOR_ADD, t, t);
         Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
         Node a = nm->mkNode(BITVECTOR_AND, sub, s);
         Node sceq = nm->mkNode(BITVECTOR_UGE, a, t);
@@ -1920,7 +1920,7 @@ Node getICBvShl(
          * min is the signed minimum value with getSize(min) = w  */
         Node min = bv::utils::mkMinSigned(w);
         Node shl = nm->mkNode(BITVECTOR_SHL, min, s);
-        Node add = nm->mkNode(BITVECTOR_PLUS, t, min);
+        Node add = nm->mkNode(BITVECTOR_ADD, t, min);
         scl = nm->mkNode(BITVECTOR_ULT, shl, add);
       }
       else
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index ec15b926f..9ffb31df3 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -184,7 +184,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
       Assert(slack.isConst());
       // remember the slack value for the asserted literal
       d_alit_to_model_slack[lit] = slack;
-      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
+      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_ADD, t, slack));
       Trace("cegqi-bv") << "Slack is " << slack << std::endl;
     }
     else
@@ -218,7 +218,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
     else
     {
       Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
-      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
+      ret = nm->mkNode(BITVECTOR_ADD, s, bv_one).eqNode(t);
     }
   }
   Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
@@ -573,7 +573,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
       return result;
     }
   }
-  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
+  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_ADD)
   {
     if (options::cegqiBvLinearize() && contains_pv[n])
     {
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index 5040125ba..9825130e5 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -166,8 +166,8 @@ Node normalizePvPlus(Node pv,
                      std::unordered_map<Node, bool>& contains_pv)
 {
   NodeManager* nm;
-  NodeBuilder nb_c(BITVECTOR_PLUS);
-  NodeBuilder nb_l(BITVECTOR_PLUS);
+  NodeBuilder nb_c(BITVECTOR_ADD);
+  NodeBuilder nb_l(BITVECTOR_ADD);
   BvLinearAttribute is_linear;
   bool neg;
 
@@ -199,7 +199,7 @@ Node normalizePvPlus(Node pv,
       nb_c << coeff;
       continue;
     }
-    else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear))
+    else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear))
     {
       Assert(isLinearPlus(nc, pv, contains_pv));
       Node coeff = utils::getPvCoeff(pv, nc[0]);
@@ -240,7 +240,7 @@ Node normalizePvPlus(Node pv,
     }
     else
     {
-      result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs);
+      result = nm->mkNode(BITVECTOR_ADD, pv_mult_coeffs, leafs);
       contains_pv[result] = true;
       result.setAttribute(is_linear, true);
     }
@@ -272,7 +272,7 @@ Node normalizePvEqual(Node pv,
     }
     if (child.getAttribute(is_linear) || child == pv)
     {
-      if (child.getKind() == BITVECTOR_PLUS)
+      if (child.getKind() == BITVECTOR_ADD)
       {
         Assert(isLinearPlus(child, pv, contains_pv));
         coeffs[i] = utils::getPvCoeff(pv, child[0]);
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index 6be22805d..4c7c096b4 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -66,7 +66,7 @@ Node normalizePvMult(TNode pv,
                      std::unordered_map<Node, bool>& contains_pv);
 
 /**
- * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
+ * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks
  * terms in which pv occurs.
  * For example,
  *
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 29194ff36..047318e86 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -131,9 +131,9 @@ class ExtendedRewriter
    * be treated as immutable. This is for instance to prevent propagation
    * beneath illegal terms. As an example:
    *   (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but
-   *   (bvand A (bvplus A B)) is not equivalent to (bvand A (bvplus 1..1 B)),
+   *   (bvand A (bvadd A B)) is not equivalent to (bvand A (bvadd 1..1 B)),
    * hence, when using this function to do BCP for bit-vectors, we have that
-   * BITVECTOR_AND is a bcp_kind, but BITVECTOR_PLUS is not.
+   * BITVECTOR_AND is a bcp_kind, but BITVECTOR_ADD is not.
    *
    * If this function returns a non-null node ret, then n ---> ret.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 263b36abf..7ee22dc5b 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -811,7 +811,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       std::vector<Kind> bin_kinds = {BITVECTOR_AND,
                                      BITVECTOR_OR,
                                      BITVECTOR_XOR,
-                                     BITVECTOR_PLUS,
+                                     BITVECTOR_ADD,
                                      BITVECTOR_SUB,
                                      BITVECTOR_MULT,
                                      BITVECTOR_UDIV,
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index b771db986..0c9cb91d7 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -287,7 +287,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry)
     }
   }
   return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
-         || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
+         || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
          || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
          || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT
          || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT
@@ -304,7 +304,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry)
     }
   }
   return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
-         || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
+         || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
          || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
          || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION
          || k == SEP_STAR;
@@ -389,7 +389,7 @@ Node TermUtil::mkTypeValueOffset(TypeNode tn,
     else if (tn.isBitVector())
     {
       val_o = Rewriter::rewrite(
-          NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
+          NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val));
     }
   }
   return val_o;
@@ -443,10 +443,8 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
   TypeNode tn = n.getType();
   if (n == mkTypeValue(tn, 0))
   {
-    if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS
-        || ik == BITVECTOR_OR
-        || ik == BITVECTOR_XOR
-        || ik == STRING_CONCAT)
+    if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_ADD
+        || ik == BITVECTOR_OR || ik == BITVECTOR_XOR || ik == STRING_CONCAT)
     {
       return true;
     }
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);
 }
 
-- 
2.30.2