BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

18 files changed, 159 insertions, 152 deletions

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]; }