From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 2 Feb 2022 22:27:14 +0000 (-0800)
Subject: Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)
X-Git-Tag: cvc5-1.0.0~471
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eab7bf6702c174c2c58373035cf9b8a099a209ae;p=cvc5.git

Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)

This renames the internal arithmetic kinds MINUS and UMINUS for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_SUB, FLOATINGPOINT_SUB).
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2105ecca0..4371bac8d 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -134,8 +134,8 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {MULT, cvc5::Kind::MULT},
     {IAND, cvc5::Kind::IAND},
     {POW2, cvc5::Kind::POW2},
-    {MINUS, cvc5::Kind::MINUS},
-    {UMINUS, cvc5::Kind::UMINUS},
+    {MINUS, cvc5::Kind::SUB},
+    {UMINUS, cvc5::Kind::NEG},
     {DIVISION, cvc5::Kind::DIVISION},
     {INTS_DIVISION, cvc5::Kind::INTS_DIVISION},
     {INTS_MODULUS, cvc5::Kind::INTS_MODULUS},
@@ -416,8 +416,8 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::MULT, MULT},
         {cvc5::Kind::IAND, IAND},
         {cvc5::Kind::POW2, POW2},
-        {cvc5::Kind::MINUS, MINUS},
-        {cvc5::Kind::UMINUS, UMINUS},
+        {cvc5::Kind::SUB, MINUS},
+        {cvc5::Kind::NEG, UMINUS},
         {cvc5::Kind::DIVISION, DIVISION},
         {cvc5::Kind::DIVISION_TOTAL, INTERNAL_KIND},
         {cvc5::Kind::INTS_DIVISION, INTS_DIVISION},
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 3082377c7..4927247bb 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -160,12 +160,12 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
             newKind = kind::BITVECTOR_MULT;
             max = max * 2;
             break;
-          case kind::MINUS:
+          case kind::SUB:
             Assert(children.size() == 2);
             newKind = kind::BITVECTOR_SUB;
             max = max + 1;
             break;
-          case kind::UMINUS:
+          case kind::NEG:
             Assert(children.size() == 1);
             newKind = kind::BITVECTOR_NEG;
             max = max + 1;
@@ -234,7 +234,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
           Node bv2int = nm->mkNode(
               kind::ITE,
               nm->mkNode(kind::BITVECTOR_SLT, result, nm->mkConst(bvzero)),
-              nm->mkNode(kind::UMINUS, negResult),
+              nm->mkNode(kind::NEG, negResult),
               nm->mkNode(kind::BITVECTOR_TO_NAT, result));
           d_preprocContext->addSubstitution(current, bv2int);
         }
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 27f34f177..aa7805284 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -60,8 +60,7 @@ Node NlExtPurify::purifyNlTerms(TNode n,
   Node ret = n;
   if (n.getNumChildren() > 0)
   {
-    if (beneathMult
-        && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
+    if (beneathMult && (n.getKind() == kind::PLUS || n.getKind() == kind::SUB))
     {
       // don't do it if it rewrites to a constant
       Node nr = rewrite(n);
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 7a58fc231..31a888dd0 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -310,7 +310,7 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::NOT:
         case kind::BITVECTOR_NOT:
         case kind::BITVECTOR_NEG:
-        case kind::UMINUS:
+        case kind::NEG:
           ++d_numUnconstrainedElim;
           Assert(parent[0] == current);
           if (currentSub.isNull())
@@ -448,7 +448,7 @@ void UnconstrainedSimplifier::processUnconstrained()
         // N-ary operators returning same type requiring at least one child to
         // be unconstrained
         case kind::PLUS:
-        case kind::MINUS:
+        case kind::SUB:
           if (current.getType().isInteger() && !parent.getType().isInteger())
           {
             break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cf85e6b0e..173247b1c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1009,8 +1009,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::ARCCOTANGENT: return "arccot";
   case kind::PI: return "real.pi";
   case kind::SQRT: return "sqrt";
-  case kind::MINUS: return "-";
-  case kind::UMINUS: return "-";
+  case kind::SUB: return "-";
+  case kind::NEG: return "-";
   case kind::LT: return "<";
   case kind::LEQ: return "<=";
   case kind::GT: return ">";
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index af683ffc6..4d1a3b5a6 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -418,12 +418,12 @@ bool AletheProofPostprocessCallback::update(Node res,
               vrule = AletheRule::PROD_SIMPLIFY;
               break;
             }
-            case kind::MINUS:
+            case kind::SUB:
             {
               vrule = AletheRule::MINUS_SIMPLIFY;
               break;
             }
-            case kind::UMINUS:
+            case kind::NEG:
             {
               vrule = AletheRule::UNARY_MINUS_SIMPLIFY;
               break;
diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 56326a2fe..ffde0b274 100644
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -292,14 +292,14 @@ Node LfscNodeConverter::postConvert(Node n)
     ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
     return nm->mkNode(APPLY_UF, f, convert(storeAll.getValue()));
   }
-  else if (k == GEQ || k == GT || k == LEQ || k == LT || k == MINUS
+  else if (k == GEQ || k == GT || k == LEQ || k == LT || k == SUB
            || k == DIVISION || k == DIVISION_TOTAL || k == INTS_DIVISION
            || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS
-           || k == INTS_MODULUS_TOTAL || k == UMINUS || k == POW
+           || k == INTS_MODULUS_TOTAL || k == NEG || k == POW
            || isIndexedOperatorKind(k))
   {
     // must give special names to SMT-LIB operators with arithmetic subtyping
-    // note that MINUS is not n-ary
+    // note that SUB is not n-ary
     // get the macro-apply version of the operator
     Node opc = getOperatorOfTerm(n, true);
     std::vector<Node> children;
@@ -983,15 +983,14 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
   }
   // all arithmetic kinds must explicitly deal with real vs int subtyping
   if (k == PLUS || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT
-      || k == LEQ || k == LT || k == MINUS || k == DIVISION
-      || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
-      || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == UMINUS
-      || k == POW)
+      || k == LEQ || k == LT || k == SUB || k == DIVISION || k == DIVISION_TOTAL
+      || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS
+      || k == INTS_MODULUS_TOTAL || k == NEG || k == POW)
   {
     // currently allow subtyping
     opName << "a.";
   }
-  if (k == UMINUS)
+  if (k == NEG)
   {
     opName << "u";
   }
diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp
index 151adc874..99a38dd58 100644
--- a/src/theory/arith/arith_poly_norm.cpp
+++ b/src/theory/arith/arith_poly_norm.cpp
@@ -201,7 +201,7 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n)
           visited[cur].addMonomial(null, r);
         }
       }
-      else if (k == PLUS || k == MINUS || k == UMINUS || k == MULT
+      else if (k == PLUS || k == SUB || k == NEG || k == MULT
                || k == NONLINEAR_MULT)
       {
         visited[cur] = PolyNorm();
@@ -225,15 +225,15 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n)
       switch (k)
       {
         case PLUS:
-        case MINUS:
-        case UMINUS:
+        case SUB:
+        case NEG:
         case MULT:
         case NONLINEAR_MULT:
           for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
           {
             it = visited.find(cur[i]);
             Assert(it != visited.end());
-            if ((k == MINUS && i == 1) || k == UMINUS)
+            if ((k == SUB && i == 1) || k == NEG)
             {
               ret.subtract(it->second);
             }
diff --git a/src/theory/arith/arith_poly_norm.h b/src/theory/arith/arith_poly_norm.h
index fafa94ee3..c36da60be 100644
--- a/src/theory/arith/arith_poly_norm.h
+++ b/src/theory/arith/arith_poly_norm.h
@@ -58,7 +58,7 @@ class PolyNorm
   bool isEqual(const PolyNorm& p) const;
   /**
    * Make polynomial from real term n. This method normalizes applications
-   * of operators PLUS, MINUS, UMINUS, MULT, and NONLINEAR_MULT only.
+   * of operators PLUS, SUB, NEG, MULT, and NONLINEAR_MULT only.
    */
   static PolyNorm mkPolyNorm(TNode n);
   /** Do a and b normalize to the same polynomial? */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index c57665948..49907450a 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -355,9 +355,9 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){
   return RewriteResponse(REWRITE_DONE, t);
 }
 
-RewriteResponse ArithRewriter::rewriteMinus(TNode t)
+RewriteResponse ArithRewriter::rewriteSub(TNode t)
 {
-  Assert(t.getKind() == kind::MINUS);
+  Assert(t.getKind() == kind::SUB);
   Assert(t.getNumChildren() == 2);
 
   auto* nm = NodeManager::currentNM();
@@ -372,8 +372,9 @@ RewriteResponse ArithRewriter::rewriteMinus(TNode t)
       nm->mkNode(Kind::PLUS, t[0], makeUnaryMinusNode(t[1])));
 }
 
-RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
-  Assert(t.getKind() == kind::UMINUS);
+RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
+{
+  Assert(t.getKind() == kind::NEG);
 
   if (t[0].isConst())
   {
@@ -405,8 +406,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   }else{
     switch(Kind k = t.getKind()){
       case kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
-      case kind::MINUS: return rewriteMinus(t);
-      case kind::UMINUS: return rewriteUMinus(t, true);
+      case kind::SUB: return rewriteSub(t);
+      case kind::NEG: return rewriteNeg(t, true);
       case kind::DIVISION:
       case kind::DIVISION_TOTAL: return rewriteDiv(t, true);
       case kind::PLUS: return preRewritePlus(t);
@@ -453,8 +454,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl;
     switch(t.getKind()){
       case kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
-      case kind::MINUS: return rewriteMinus(t);
-      case kind::UMINUS: return rewriteUMinus(t, false);
+      case kind::SUB: return rewriteSub(t);
+      case kind::NEG: return rewriteNeg(t, false);
       case kind::DIVISION:
       case kind::DIVISION_TOTAL: return rewriteDiv(t, false);
       case kind::PLUS: return postRewritePlus(t);
@@ -801,7 +802,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
       }
       else if (rat.sgn() == -1)
       {
-        Node ret = nm->mkNode(kind::UMINUS,
+        Node ret = nm->mkNode(kind::NEG,
                               nm->mkNode(kind::SINE, nm->mkConstReal(-rat)));
         return RewriteResponse(REWRITE_AGAIN_FULL, ret);
       }
@@ -851,10 +852,8 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
               kind::INTS_DIVISION, mkRationalNode(r_abs + rone), ntwo);
           Node new_pi_factor;
           if( r.sgn()==1 ){
-            new_pi_factor =
-                nm->mkNode(kind::MINUS,
-                           pi_factor,
-                           nm->mkNode(kind::MULT, ntwo, ra_div_two));
+            new_pi_factor = nm->mkNode(
+                kind::SUB, pi_factor, nm->mkNode(kind::MULT, ntwo, ra_div_two));
           }else{
             Assert(r.sgn() == -1);
             new_pi_factor =
@@ -882,7 +881,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
           {
             return RewriteResponse(
                 REWRITE_AGAIN_FULL,
-                nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, rem)));
+                nm->mkNode(kind::NEG, nm->mkNode(kind::SINE, rem)));
           }
         }
         else if (rem.isNull())
@@ -917,7 +916,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
         REWRITE_AGAIN_FULL,
         nm->mkNode(
             kind::SINE,
-            nm->mkNode(kind::MINUS,
+            nm->mkNode(kind::SUB,
                        nm->mkNode(kind::MULT,
                                   nm->mkConstReal(Rational(1) / Rational(2)),
                                   mkPi()),
@@ -1164,7 +1163,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre)
     // (mod x (- c)) ---> (mod x c)
     Node nn = nm->mkNode(k, t[0], nm->mkConstInt(-t[1].getConst<Rational>()));
     Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL)
-                   ? nm->mkNode(kind::UMINUS, nn)
+                   ? nm->mkNode(kind::NEG, nn)
                    : nn;
     return returnRewrite(t, ret, Rewrite::DIV_MOD_PULL_NEG_DEN);
   }
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 90140cc18..072894000 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -56,8 +56,8 @@ class ArithRewriter : public TheoryRewriter
   static RewriteResponse rewriteRAN(TNode t);
   static RewriteResponse rewriteVariable(TNode t);
 
-  static RewriteResponse rewriteMinus(TNode t);
-  static RewriteResponse rewriteUMinus(TNode t, bool pre);
+  static RewriteResponse rewriteSub(TNode t);
+  static RewriteResponse rewriteNeg(TNode t, bool pre);
   static RewriteResponse rewriteDiv(TNode t, bool pre);
   static RewriteResponse rewriteAbs(TNode t);
   static RewriteResponse rewriteIntsDivMod(TNode t, bool pre);
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index ba326ba56..5d96e019f 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -15,8 +15,8 @@ rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
 operator PLUS 2: "arithmetic addition (N-ary)"
 operator MULT 2: "arithmetic multiplication (N-ary)"
 operator NONLINEAR_MULT 2: "synonym for MULT"
-operator MINUS 2 "arithmetic binary subtraction operator"
-operator UMINUS 1 "arithmetic unary negation"
+operator SUB 2 "arithmetic binary subtraction operator"
+operator NEG 1 "arithmetic unary negation"
 operator DIVISION 2 "real division, division by 0 undefined (user symbol)"
 operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)"
 operator INTS_DIVISION 2 "integer division, division by 0 undefined (user symbol)"
@@ -121,8 +121,8 @@ operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used inter
 typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule
-typerule MINUS ::cvc5::theory::arith::ArithOperatorTypeRule
-typerule UMINUS ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule SUB ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule NEG ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule
 
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index a16ffdd02..887ef3f1b 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -717,7 +717,7 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
     {
       return a_eq_b;
     }
-    Node negate_b = NodeManager::currentNM()->mkNode(Kind::UMINUS, b);
+    Node negate_b = NodeManager::currentNM()->mkNode(Kind::NEG, b);
     return a_eq_b.orNode(a.eqNode(negate_b));
   }
   else if (status < 0)
@@ -734,8 +734,8 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
   // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) );
   Node a_is_nonnegative = nm->mkNode(Kind::GEQ, a, d_data->d_zero);
   Node b_is_nonnegative = nm->mkNode(Kind::GEQ, b, d_data->d_zero);
-  Node negate_a = nm->mkNode(Kind::UMINUS, a);
-  Node negate_b = nm->mkNode(Kind::UMINUS, b);
+  Node negate_a = nm->mkNode(Kind::NEG, a);
+  Node negate_b = nm->mkNode(Kind::NEG, b);
   return a_is_nonnegative.iteNode(
       b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b),
                                nm->mkNode(greater_op, a, negate_b)),
diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
index ff6d6a5e8..fe134abb4 100644
--- a/src/theory/arith/nl/ext/proof_checker.cpp
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -136,7 +136,7 @@ Node ExtProofRuleChecker::checkInternal(PfRule id,
     Node b = args[4];
     int sgn = args[5].getConst<Rational>().getNumerator().sgn();
     Assert(sgn == -1 || sgn == 1);
-    Node tplane = nm->mkNode(Kind::MINUS,
+    Node tplane = nm->mkNode(Kind::SUB,
                              nm->mkNode(Kind::PLUS,
                                         nm->mkNode(Kind::MULT, b, x),
                                         nm->mkNode(Kind::MULT, a, y)),
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index fbf8caf6a..4ec1f2ca2 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -119,7 +119,7 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
             Node b_v = pts[1][p];
 
             // tangent plane
-            Node tplane = nm->mkNode(Kind::MINUS,
+            Node tplane = nm->mkNode(Kind::SUB,
                                      nm->mkNode(Kind::PLUS,
                                                 nm->mkNode(Kind::MULT, b_v, a),
                                                 nm->mkNode(Kind::MULT, a_v, b)),
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index c661dab4b..dc6b9c9d7 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -220,7 +220,7 @@ Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const
 Node IAndSolver::mkINot(unsigned k, Node x) const
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x);
+  Node ret = nm->mkNode(SUB, d_iandUtils.twoToKMinusOne(k), x);
   ret = rewrite(ret);
   return ret;
 }
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 700eb6de9..d64c19963 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -267,7 +267,7 @@ Node IAndUtils::twoToKMinusOne(unsigned k) const
 {
   // could be faster
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(kind::MINUS, twoToK(k), d_one);
+  return nm->mkNode(kind::SUB, twoToK(k), d_one);
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 90138bf3e..1f50290c1 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -676,7 +676,7 @@ bool NlModel::simpleCheckModelLit(Node lit)
         Trace("nl-ext-cms-debug") << "    b = " << b << std::endl;
         // find maximal/minimal value on the interval
         Node apex = nm->mkNode(
-            DIVISION, nm->mkNode(UMINUS, b), nm->mkNode(MULT, d_two, a));
+            DIVISION, nm->mkNode(NEG, b), nm->mkNode(MULT, d_two, a));
         apex = rewrite(apex);
         Assert(apex.isConst());
         // for lower, upper, whether we are greater than the apex
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 77e5f9f3f..3992c31f6 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -264,7 +264,7 @@ std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e,
   {
     // pick c-1
     bounds.first = rewrite(
-        NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one));
+        NodeManager::currentNM()->mkNode(Kind::SUB, center, d_data->d_one));
   }
   if (bounds.second.isNull())
   {
diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index 3bf1ace98..cbf867ef4 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.cpp
+++ b/src/theory/arith/nl/transcendental/proof_checker.cpp
@@ -51,9 +51,9 @@ Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
                     evall,
                     nm->mkNode(Kind::MULT,
                                nm->mkNode(Kind::DIVISION,
-                                          nm->mkNode(Kind::MINUS, evall, evalu),
-                                          nm->mkNode(Kind::MINUS, l, u)),
-                               nm->mkNode(Kind::MINUS, t, l)));
+                                          nm->mkNode(Kind::SUB, evall, evalu),
+                                          nm->mkNode(Kind::SUB, l, u)),
+                               nm->mkNode(Kind::SUB, t, l)));
 }
 
 }  // namespace
@@ -271,10 +271,10 @@ Node TranscendentalProofRuleChecker::checkInternal(
         AND,
         nm->mkNode(IMPLIES,
                    nm->mkNode(GT, args[0], mpi),
-                   nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))),
+                   nm->mkNode(GT, s, nm->mkNode(SUB, mpi, args[0]))),
         nm->mkNode(IMPLIES,
                    nm->mkNode(LT, args[0], pi),
-                   nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0]))));
+                   nm->mkNode(LT, s, nm->mkNode(SUB, pi, args[0]))));
   }
   else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG)
   {
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index d574a9572..3c5ae8006 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -189,13 +189,12 @@ void SineSolver::checkInitialRefine()
                   nm->mkNode(Kind::GT, t[0], d_data->d_pi_neg),
                   nm->mkNode(Kind::GT,
                              t,
-                             nm->mkNode(Kind::MINUS, d_data->d_pi_neg, t[0]))),
+                             nm->mkNode(Kind::SUB, d_data->d_pi_neg, t[0]))),
               nm->mkNode(
                   Kind::IMPLIES,
                   nm->mkNode(Kind::LT, t[0], d_data->d_pi),
-                  nm->mkNode(Kind::LT,
-                             t,
-                             nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))));
+                  nm->mkNode(
+                      Kind::LT, t, nm->mkNode(Kind::SUB, d_data->d_pi, t[0]))));
           CDProof* proof = nullptr;
           if (d_data->isProofEnabled())
           {
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index c9e0015e2..5afe3a705 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -121,7 +121,7 @@ void TaylorGenerator::getPolynomialApproximationBounds(
     else
     {
       Assert(k == Kind::SINE);
-      Node l = nm->mkNode(Kind::MINUS, taylor_sum, ru);
+      Node l = nm->mkNode(Kind::SUB, taylor_sum, ru);
       Node u = nm->mkNode(Kind::PLUS, taylor_sum, ru);
       pbounds.d_lower = l;
       pbounds.d_upperNeg = u;
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index e32f336ac..fd5f7d07a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -268,7 +268,7 @@ Node TranscendentalState::mkSecantPlane(
 {
   NodeManager* nm = NodeManager::currentNM();
   // Figure 3: S_l( x ), S_u( x ) for s = 0,1
-  Node rcoeff_n = rewrite(nm->mkNode(Kind::MINUS, lower, upper));
+  Node rcoeff_n = rewrite(nm->mkNode(Kind::SUB, lower, upper));
   Assert(rcoeff_n.isConst());
   Rational rcoeff = rcoeff_n.getConst<Rational>();
   Assert(rcoeff.sgn() != 0);
@@ -277,9 +277,9 @@ Node TranscendentalState::mkSecantPlane(
                  lval,
                  nm->mkNode(Kind::MULT,
                             nm->mkNode(Kind::DIVISION,
-                                       nm->mkNode(Kind::MINUS, lval, uval),
-                                       nm->mkNode(Kind::MINUS, lower, upper)),
-                            nm->mkNode(Kind::MINUS, arg, lower)));
+                                       nm->mkNode(Kind::SUB, lval, uval),
+                                       nm->mkNode(Kind::SUB, lower, upper)),
+                            nm->mkNode(Kind::SUB, arg, lower)));
   Trace("nl-trans") << "Creating secant plane for transcendental function of "
                     << arg << std::endl;
   Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( "
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index f346d7596..ab98f67ac 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -124,7 +124,7 @@ Node OperatorElim::eliminateOperators(Node node,
           bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
       Node one = nm->mkConstReal(Rational(1));
       Node zero = nm->mkConstReal(Rational(0));
-      Node diff = nm->mkNode(MINUS, node[0], v);
+      Node diff = nm->mkNode(SUB, node[0], v);
       Node lem = mkInRange(diff, zero, one);
       Node toIntSkolem =
           mkWitnessTerm(v,
@@ -227,7 +227,7 @@ Node OperatorElim::eliminateOperators(Node node,
           v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
       if (k == INTS_MODULUS_TOTAL)
       {
-        Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
+        Node nn = nm->mkNode(SUB, num, nm->mkNode(MULT, den, intVar));
         return nn;
       }
       else
@@ -320,7 +320,7 @@ Node OperatorElim::eliminateOperators(Node node,
           nm->mkNode(LT,
                      node[0],
                      nm->mkConstRealOrInt(node[0].getType(), Rational(0))),
-          nm->mkNode(UMINUS, node[0]),
+          nm->mkNode(NEG, node[0]),
           node[0]);
       break;
     }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 61dbe4fce..60f925e75 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -342,7 +342,7 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
   {
     return d_internal->getEqualityStatus(a,b);
   }
-  Node diff = d_env.getNodeManager()->mkNode(Kind::MINUS, a, b);
+  Node diff = d_env.getNodeManager()->mkNode(Kind::SUB, a, b);
   std::optional<bool> isZero = isExpressionZero(d_env, diff, d_arithModelCache);
   if (isZero)
   {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4efdfc2bf..572af7fb3 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3782,10 +3782,12 @@ DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const
       }
       return value;
     }
-    case kind::MINUS: {  // 2 args
+    case kind::SUB:
+    {  // 2 args
       return getDeltaValue(term[0]) - getDeltaValue(term[1]);
     }
-    case kind::UMINUS: {  // 1 arg
+    case kind::NEG:
+    {  // 1 arg
       return (-getDeltaValue(term[0]));
     }
 
@@ -4878,8 +4880,7 @@ bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational&
   success = decomposeTerm(rewrite(right), rm, rp, rc);
   if(!success){ return false; }
 
-  Node diff =
-      rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right));
+  Node diff = rewrite(NodeManager::currentNM()->mkNode(kind::SUB, left, right));
   Rational dc;
   success = decomposeTerm(diff, dm, dp, dc);
   Assert(success);
diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp
index a6895e4b1..4e4b75c09 100644
--- a/src/theory/bags/bag_reduction.cpp
+++ b/src/theory/bags/bag_reduction.cpp
@@ -87,7 +87,7 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector<Node>& asserts)
     Node i =
         bvm->mkBoundVar<FirstIndexVarAttribute>(node, "i", nm->integerType());
     Node iList = nm->mkNode(BOUND_VAR_LIST, i);
-    Node iMinusOne = nm->mkNode(MINUS, i, one);
+    Node iMinusOne = nm->mkNode(SUB, i, one);
     Node uf_i = nm->mkNode(APPLY_UF, uf, i);
     Node combine_0 = nm->mkNode(APPLY_UF, combine, zero);
     Node combine_iMinusOne = nm->mkNode(APPLY_UF, combine, iMinusOne);
@@ -158,7 +158,7 @@ Node BagReduction::reduceCardOperator(Node node, std::vector<Node>& asserts)
       bvm->mkBoundVar<SecondIndexVarAttribute>(node, "j", nm->integerType());
   Node iList = nm->mkNode(BOUND_VAR_LIST, i);
   Node jList = nm->mkNode(BOUND_VAR_LIST, j);
-  Node iMinusOne = nm->mkNode(MINUS, i, one);
+  Node iMinusOne = nm->mkNode(SUB, i, one);
   Node uf_i = nm->mkNode(APPLY_UF, uf, i);
   Node uf_j = nm->mkNode(APPLY_UF, uf, j);
   Node cardinality_0 = nm->mkNode(APPLY_UF, cardinality, zero);
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 3247548c5..248f0337e 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -262,7 +262,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
   Node skolem = getSkolem(n, inferInfo);
   Node count = getMultiplicityTerm(e, skolem);
 
-  Node subtract = d_nm->mkNode(MINUS, countA, countB);
+  Node subtract = d_nm->mkNode(SUB, countA, countB);
   Node gte = d_nm->mkNode(GEQ, countA, countB);
   Node difference = d_nm->mkNode(ITE, gte, subtract, d_zero);
   Node equal = count.eqNode(difference);
@@ -447,7 +447,7 @@ std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n,
   Node iList = d_nm->mkNode(BOUND_VAR_LIST, i);
   Node jList = d_nm->mkNode(BOUND_VAR_LIST, j);
   Node iPlusOne = d_nm->mkNode(PLUS, i, d_one);
-  Node iMinusOne = d_nm->mkNode(MINUS, i, d_one);
+  Node iMinusOne = d_nm->mkNode(SUB, i, d_one);
   Node uf_i = d_nm->mkNode(APPLY_UF, uf, i);
   Node uf_j = d_nm->mkNode(APPLY_UF, uf, j);
   Node f_uf_i = d_nm->mkNode(APPLY_UF, f, uf_i);
diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index b761a5dcd..f69ca7854 100644
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -303,7 +303,7 @@ Node IntBlaster::translateWithChildren(
       returnNode = d_nm->mkNode(
           kind::ITE,
           d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
-          d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
+          d_nm->mkNode(kind::SUB, pow2BvSize, d_one),
           divNode);
       break;
     }
@@ -598,7 +598,7 @@ Node IntBlaster::uts(Node x, uint64_t bvsize)
   Node modNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, x, powNode);
   Node two = d_nm->mkConstInt(Rational(2));
   Node twoTimesNode = d_nm->mkNode(kind::MULT, two, modNode);
-  return d_nm->mkNode(kind::MINUS, twoTimesNode, x);
+  return d_nm->mkNode(kind::SUB, twoTimesNode, x);
 }
 
 Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount)
@@ -1064,7 +1064,7 @@ Node IntBlaster::createBVOrNode(Node x,
 
 Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize)
 {
-  Node minus = d_nm->mkNode(kind::MINUS, x, y);
+  Node minus = d_nm->mkNode(kind::SUB, x, y);
   Node p2 = pow2(bvsize);
   return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2);
 }
@@ -1081,12 +1081,12 @@ Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize)
   // Based on Hacker's Delight section 2-2 equation a:
   // -x = ~x+1
   Node p2 = pow2(bvsize);
-  return d_nm->mkNode(kind::MINUS, p2, n);
+  return d_nm->mkNode(kind::SUB, p2, n);
 }
 
 Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize)
 {
-  return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
+  return d_nm->mkNode(kind::SUB, maxInt(bvsize), n);
 }
 
 }  // namespace cvc5
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 1134c0a5a..2ec6dfe1b 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -701,7 +701,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
   if (doSymBreak)
   {
     // direct solving for children
-    //   for instance, we may want to insist that the LHS of MINUS is 0
+    //   for instance, we may want to insist that the LHS of SUB is 0
     Trace("sygus-sb-simple-debug") << "  Solve children..." << std::endl;
     std::map<unsigned, unsigned> children_solved;
     for (unsigned j = 0; j < dt_index_nargs; j++)
@@ -747,7 +747,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
           {
             // other cases of rewriting x k x -> x'
             Node req_const;
-            if (nk == GT || nk == LT || nk == XOR || nk == MINUS
+            if (nk == GT || nk == LT || nk == XOR || nk == SUB
                 || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR
                 || nk == BITVECTOR_UREM)
             {
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index 4826e87bc..c819218ce 100644
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -200,7 +200,7 @@ bool SygusSimpleSymBreak::considerArgKind(
   Assert(rt.empty());
 
   // construct rt by cases
-  if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
+  if (pk == NOT || pk == BITVECTOR_NOT || pk == NEG || pk == BITVECTOR_NEG)
   {
     // negation normal form
     if (pk == k)
@@ -280,12 +280,12 @@ bool SygusSimpleSymBreak::considerArgKind(
           rt.d_req_kind = BITVECTOR_XNOR;
         }
       }
-      else if (pk == UMINUS)
+      else if (pk == NEG)
       {
         if (k == PLUS)
         {
           rt.d_req_kind = PLUS;
-          reqk = UMINUS;
+          reqk = NEG;
         }
       }
       else if (pk == BITVECTOR_NEG)
@@ -327,17 +327,17 @@ bool SygusSimpleSymBreak::considerArgKind(
       }
     }
   }
-  else if (k == MINUS || k == BITVECTOR_SUB)
+  else if (k == SUB || k == BITVECTOR_SUB)
   {
-    if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
-        || pk == LT || pk == GEQ || pk == GT)
+    if (pk == EQUAL || pk == SUB || pk == BITVECTOR_SUB || pk == LEQ || pk == LT
+        || pk == GEQ || pk == GT)
     {
       int oarg = arg == 0 ? 1 : 0;
       //  (~ x (- y z))  ---->  (~ (+ x z) y)
       //  (~ (- 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_ADD;
+      rt.d_children[oarg].d_req_kind = k == SUB ? 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);
     }
@@ -345,7 +345,7 @@ bool SygusSimpleSymBreak::considerArgKind(
     {
       //  (+ x (- y z))  -----> (- (+ x y) z)
       //  (+ (- y z) x)  -----> (- (+ x y) z)
-      rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
+      rt.d_req_kind = pk == PLUS ? SUB : BITVECTOR_SUB;
       int oarg = arg == 0 ? 1 : 0;
       rt.d_children[0].d_req_kind = pk;
       rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 6b4176c13..1ab234ae9 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -427,7 +427,7 @@ EvalResult Evaluator::evalInternal(
           break;
         }
 
-        case kind::MINUS:
+        case kind::SUB:
         {
           const Rational& x = results[currNode[0]].d_rat;
           const Rational& y = results[currNode[1]].d_rat;
@@ -435,7 +435,7 @@ EvalResult Evaluator::evalInternal(
           break;
         }
 
-        case kind::UMINUS:
+        case kind::NEG:
         {
           const Rational& x = results[currNode[0]].d_rat;
           results[currNode] = EvalResult(-x);
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index ecf2d9a48..6528959c3 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -291,8 +291,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
       else
       {
         Node delta = d_vtc->getVtsDelta();
-        uval = nm->mkNode(
-            uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta);
+        uval =
+            nm->mkNode(uires == CEG_TT_UPPER_STRICT ? PLUS : SUB, uval, delta);
         uval = rewrite(uval);
       }
     }
@@ -363,7 +363,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         // could get rho value for infinity here
         if (rr == 0)
         {
-          val = nm->mkNode(UMINUS, val);
+          val = nm->mkNode(NEG, val);
           val = rewrite(val);
         }
         TermProperties pv_prop_no_bound;
@@ -623,7 +623,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       }
       else if (!vals[1].isNull())
       {
-        val = nm->mkNode(MINUS, vals[1], d_one);
+        val = nm->mkNode(SUB, vals[1], d_one);
         val = rewrite(val);
       }
     }
@@ -933,8 +933,8 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
           (msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
                                                                           : -1;
       val = rewrite(
-          nm->mkNode(ires_use == -1 ? PLUS : MINUS,
-                     nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart),
+          nm->mkNode(ires_use == -1 ? PLUS : SUB,
+                     nm->mkNode(ires_use == -1 ? SUB : PLUS, val, realPart),
                      nm->mkNode(TO_INTEGER, realPart)));
       // could round up for upper bounds here
       Trace("cegqi-arith-debug") << "result : " << val << std::endl;
@@ -1001,11 +1001,11 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
     Node rho;
     if (isLower)
     {
-      rho = nm->mkNode(MINUS, ceValue, mt);
+      rho = nm->mkNode(SUB, ceValue, mt);
     }
     else
     {
-      rho = nm->mkNode(MINUS, mt, ceValue);
+      rho = nm->mkNode(SUB, mt, ceValue);
     }
     rho = rewrite(rho);
     Trace("cegqi-arith-bound2")
@@ -1015,7 +1015,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
     rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta);
     rho = rewrite(rho);
     Trace("cegqi-arith-bound2") << rho << std::endl;
-    Kind rk = isLower ? PLUS : MINUS;
+    Kind rk = isLower ? PLUS : SUB;
     val = nm->mkNode(rk, val, rho);
     val = rewrite(val);
     Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 45ac899e1..bd3f616d6 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1272,7 +1272,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
         atom_lhs = atom[0];
         atom_rhs = atom[1];
       }else{
-        atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
+        atom_lhs = nm->mkNode(SUB, atom[0], atom[1]);
         atom_lhs = rewrite(atom_lhs);
         atom_rhs = nm->mkConstRealOrInt(atom_lhs.getType(), Rational(0));
       }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index ab4bbc91b..fe852a90c 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -364,8 +364,8 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
     {
       if (pat.getKind() == GT)
       {
-        t_match = nm->mkNode(
-            MINUS, t, nm->mkConstRealOrInt(t.getType(), Rational(1)));
+        t_match =
+            nm->mkNode(SUB, t, nm->mkConstRealOrInt(t.getType(), Rational(1)));
       }else{
         t_match = t;
       }
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index e4d7436c8..e792faa5f 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -671,7 +671,7 @@ Node PatternTermSelector::getInversion(Node n, Node x)
       {
         if (nk == PLUS)
         {
-          x = nm->mkNode(MINUS, x, nc);
+          x = nm->mkNode(SUB, x, nc);
         }
         else if (nk == MULT)
         {
@@ -685,7 +685,7 @@ Node PatternTermSelector::getInversion(Node n, Node x)
             }
             if (nc.getConst<Rational>().sgn() < 0)
             {
-              x = nm->mkNode(UMINUS, x);
+              x = nm->mkNode(NEG, x);
             }
           }
           else
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 5c0283863..54fa24c76 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -369,7 +369,7 @@ void BoundedIntegers::checkOwnership(Node f)
                      != bound_int_range_term[b].end());
               d_bounds[b][f][v] = bound_int_range_term[b][v];
             }
-            Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]);
+            Node r = nm->mkNode(SUB, d_bounds[1][f][v], d_bounds[0][f][v]);
             d_range[f][v] = rewrite(r);
             Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
           }
@@ -814,7 +814,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
       }else{
         NodeManager* nm = NodeManager::currentNM();
         Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl;
-        Node range = rewrite(nm->mkNode(MINUS, u, l));
+        Node range = rewrite(nm->mkNode(SUB, u, l));
         // 9999 is an arbitrary range past which we do not do exhaustive
         // bounded instantation, based on the check below.
         Node ra =
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e1bebee74..f87b1ab2c 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -836,7 +836,7 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
               {
                 Kind kn = k;
                 if( d_vars[index].getKind()==PLUS ){
-                  kn = MINUS;
+                  kn = SUB;
                 }
                 if( kn!=k ){
                   sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 67df20694..f1260eb69 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -932,7 +932,7 @@ Node QuantifiersRewriter::getVarElimEqString(Node lit,
               STRING_SUBSTR,
               slv,
               tpreL,
-              nm->mkNode(MINUS, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
+              nm->mkNode(SUB, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
           // forall x. r ++ x ++ t = s => P( x )
           //   is equivalent to
           // r ++ s' ++ t = s => P( s' ) where
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 6399340aa..fdd5fa0ac 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -288,7 +288,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
       Node icond = nm->mkNode(GEQ, k, nm->mkConstInt(Rational(0)));
       Node iret =
           ret.substitute(ind_vars[0],
-                         nm->mkNode(MINUS, k, nm->mkConstInt(Rational(1))))
+                         nm->mkNode(SUB, k, nm->mkConstInt(Rational(1))))
               .negate();
       n_str_ind = nm->mkNode(OR, icond.negate(), iret);
       n_str_ind = nm->mkNode(AND, icond, n_str_ind);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 13f52a12f..dc7b3d5e9 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -773,8 +773,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
 
     if (types[i].isRealOrInt())
     {
-      // Add PLUS, MINUS
-      Kind kinds[2] = {PLUS, MINUS};
+      // Add PLUS, SUB
+      Kind kinds[2] = {PLUS, SUB};
       for (const Kind kind : kinds)
       {
         Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index e1491936a..2d0561462 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -610,7 +610,7 @@ Node SygusSampler::getRandomValue(TypeNode tn)
       if (Random::getRandom().pickWithProb(0.5))
       {
         // negative
-        ret = nm->mkNode(kind::UMINUS, ret);
+        ret = nm->mkNode(kind::NEG, ret);
       }
       ret = d_env.getRewriter()->rewrite(ret);
       Assert(ret.isConst());
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 5bd22f986..23372b794 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -263,7 +263,7 @@ Node TermUtil::mkNegate(Kind notk, Node n)
 
 bool TermUtil::isNegate(Kind k)
 {
-  return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS;
+  return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == NEG;
 }
 
 bool TermUtil::isAssoc(Kind k, bool reqNAry)
@@ -437,7 +437,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
     {
       return true;
     }
-    else if (ik == MINUS || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR
+    else if (ik == SUB || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR
              || ik == BITVECTOR_ASHR || ik == BITVECTOR_SUB
              || ik == BITVECTOR_UREM)
     {
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index cb9b26731..9cf2a908d 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -282,7 +282,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     else if (node[0].getKind() == kind::SET_UNION)
     {
       Node ret = NodeManager::currentNM()->mkNode(
-          kind::MINUS,
+          kind::SUB,
           NodeManager::currentNM()->mkNode(
               kind::PLUS,
               NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]),
@@ -296,7 +296,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     else if (node[0].getKind() == kind::SET_MINUS)
     {
       Node ret = NodeManager::currentNM()->mkNode(
-          kind::MINUS,
+          kind::SUB,
           NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]),
           NodeManager::currentNM()->mkNode(
               kind::SET_CARD,
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index 0659a2ff9..46d89520b 100644
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -54,7 +54,7 @@ bool ArithEntail::check(Node a, Node b, bool strict)
   {
     return !strict;
   }
-  Node diff = NodeManager::currentNM()->mkNode(kind::MINUS, a, b);
+  Node diff = NodeManager::currentNM()->mkNode(kind::SUB, a, b);
   return check(diff, strict);
 }
 
@@ -76,10 +76,9 @@ bool ArithEntail::check(Node a, bool strict)
     return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
   }
 
-  Node ar =
-      strict ? NodeManager::currentNM()->mkNode(
-          kind::MINUS, a, NodeManager::currentNM()->mkConstInt(Rational(1)))
-             : a;
+  Node ar = strict ? NodeManager::currentNM()->mkNode(
+                kind::SUB, a, NodeManager::currentNM()->mkConstInt(Rational(1)))
+                   : a;
   ar = d_rr->rewrite(ar);
 
   if (ar.getAttribute(StrCheckEntailArithComputedAttr()))
@@ -417,7 +416,7 @@ void ArithEntail::getArithApproximations(Node a,
         {
           // n <= len( x ) implies
           //   len( x ) - n >= len( substr( x, n, m ) )
-          approx.push_back(nm->mkNode(MINUS, lenx, a[0][1]));
+          approx.push_back(nm->mkNode(SUB, lenx, a[0][1]));
         }
         else
         {
@@ -438,7 +437,7 @@ void ArithEntail::getArithApproximations(Node a,
         //   len(x)-n <= len( substr( x, n, m ) )
         if (check(a[0][1]) && check(npm, lenx))
         {
-          approx.push_back(nm->mkNode(MINUS, lenx, a[0][1]));
+          approx.push_back(nm->mkNode(SUB, lenx, a[0][1]));
         }
       }
     }
@@ -474,7 +473,7 @@ void ArithEntail::getArithApproximations(Node a,
         else
         {
           // len( x ) - len( y ) <= len( replace( x, y, z ) )
-          approx.push_back(nm->mkNode(MINUS, lenx, leny));
+          approx.push_back(nm->mkNode(SUB, lenx, leny));
         }
       }
     }
@@ -524,7 +523,7 @@ void ArithEntail::getArithApproximations(Node a,
       {
         // len( x ) >= len( y ) implies
         //   len( x ) - len( y ) >= indexof( x, y, n )
-        approx.push_back(nm->mkNode(MINUS, lenx, leny));
+        approx.push_back(nm->mkNode(SUB, lenx, leny));
       }
       else
       {
@@ -577,7 +576,7 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
     toVisit.pop_back();
 
     if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT
-        || curr.getKind() == kind::MINUS || curr.getKind() == kind::EQUAL)
+        || curr.getKind() == kind::SUB || curr.getKind() == kind::EQUAL)
     {
       for (const auto& currChild : curr)
       {
@@ -660,8 +659,7 @@ bool ArithEntail::checkWithAssumption(Node assumption,
       // (not (>= s t)) --> (>= (t - 1) s)
       Assert(assumption.getKind() == kind::NOT
              && assumption[0].getKind() == kind::GEQ);
-      x = nm->mkNode(
-          kind::MINUS, assumption[0][1], nm->mkConstInt(Rational(1)));
+      x = nm->mkNode(kind::SUB, assumption[0][1], nm->mkConstInt(Rational(1)));
       y = assumption[0][0];
     }
 
@@ -671,7 +669,7 @@ bool ArithEntail::checkWithAssumption(Node assumption,
         nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen)));
   }
 
-  Node diff = nm->mkNode(kind::MINUS, a, b);
+  Node diff = nm->mkNode(kind::SUB, a, b);
   bool res = false;
   if (assumption.isConst())
   {
diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp
index c7e72c11f..58d1efaf7 100644
--- a/src/theory/strings/array_core_solver.cpp
+++ b/src/theory/strings/array_core_solver.cpp
@@ -237,7 +237,7 @@ void ArrayCoreSolver::check(const std::vector<Node>& nthTerms,
       Node i = n[1];
       Node sLen = nm->mkNode(STRING_LENGTH, s);
       Node iRev = nm->mkNode(
-          MINUS, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
+          SUB, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
 
       std::vector<Node> nexp;
       nexp.push_back(nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), i));
diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index 90725bd2a..d7663170a 100644
--- a/src/theory/strings/array_solver.cpp
+++ b/src/theory/strings/array_solver.cpp
@@ -267,7 +267,7 @@ void ArraySolver::checkTerm(Node t, bool checkInv)
     if (!lacc.empty())
     {
       currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc);
-      currIndex = nm->mkNode(MINUS, currIndex, currSum);
+      currIndex = nm->mkNode(SUB, currIndex, currSum);
     }
     Node cc;
     if (k == STRING_UPDATE && checkInv)
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index ee54b0fce..f2fe97c7b 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -834,7 +834,7 @@ Node CoreSolver::getDecomposeConclusion(Node x,
 {
   Assert(l.getType().isInteger());
   NodeManager* nm = NodeManager::currentNM();
-  Node n = isRev ? nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), l) : l;
+  Node n = isRev ? nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), l) : l;
   Node sk1 = skc->mkSkolemCached(x, n, SkolemCache::SK_PREFIX, "dc_spt1");
   newSkolems.push_back(sk1);
   Node sk2 = skc->mkSkolemCached(x, n, SkolemCache::SK_SUFFIX_REM, "dc_spt2");
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index a638d6009..a94f09cb7 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -160,7 +160,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         Node ppSum = childLengthsPostPivot.size() == 1
                          ? childLengthsPostPivot[0]
                          : nm->mkNode(PLUS, childLengthsPostPivot);
-        currEnd = nm->mkNode(MINUS, lenx, ppSum);
+        currEnd = nm->mkNode(SUB, lenx, ppSum);
       }
       else
       {
@@ -312,7 +312,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         //        ... ^ "B" = substr( x, len( x ) - 3, 1 )  ^ ...
         Node sc = sep_children.back();
         Node lenSc = nm->mkNode(STRING_LENGTH, sc);
-        Node loc = nm->mkNode(MINUS, lenx, nm->mkNode(PLUS, lenSc, cEnd));
+        Node loc = nm->mkNode(SUB, lenx, nm->mkNode(PLUS, lenSc, cEnd));
         Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc));
         // We also must ensure that we fit. This constraint is necessary in
         // addition to the constraint above. Take this example:
@@ -415,7 +415,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP);
       Node s = c[0];
       Node lens = nm->mkNode(STRING_LENGTH, s);
-      Node sss = r == 0 ? zero : nm->mkNode(MINUS, lenx, lens);
+      Node sss = r == 0 ? zero : nm->mkNode(SUB, lenx, lens);
       Node ss = nm->mkNode(STRING_SUBSTR, x, sss, lens);
       sConstraints.push_back(ss.eqNode(s));
       if (r == 0)
@@ -428,7 +428,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         Node bound = nm->mkNode(GEQ, sss, sStartIndex);
         sConstraints.push_back(bound);
       }
-      sLength = nm->mkNode(MINUS, sLength, lens);
+      sLength = nm->mkNode(SUB, sLength, lens);
     }
     if (r == 1 && !sConstraints.empty())
     {
@@ -470,7 +470,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       }
       else if (i + 1 == nchildren)
       {
-        k = nm->mkNode(MINUS, lenx, lens);
+        k = nm->mkNode(SUB, lenx, lens);
       }
       else
       {
@@ -481,7 +481,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         Node bound =
             nm->mkNode(AND,
                        nm->mkNode(LEQ, zero, k),
-                       nm->mkNode(LEQ, k, nm->mkNode(MINUS, lenx, lens)));
+                       nm->mkNode(LEQ, k, nm->mkNode(SUB, lenx, lens)));
         echildren.push_back(bound);
       }
       Node substrEq = nm->mkNode(STRING_SUBSTR, x, k, lens).eqNode(s);
@@ -503,7 +503,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         Node ks = nm->mkNode(PLUS, k, lens);
         Node substrSuffix = nm->mkNode(
             STRING_IN_REGEXP,
-            nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(MINUS, lenx, ks)),
+            nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(SUB, lenx, ks)),
             rps);
         echildren.push_back(substrSuffix);
       }
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index eb6d2d355..2b6c4a697 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -929,7 +929,7 @@ Node RegExpOpr::reduceRegExpNeg(Node mem)
         nm->mkNode(AND, nm->mkNode(GT, b1, zero), nm->mkNode(GEQ, lens, b1));
     // internal
     Node s1 = nm->mkNode(STRING_SUBSTR, s, zero, b1);
-    Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+    Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(SUB, lens, b1));
     Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[0]).negate();
     Node s2r2 = nm->mkNode(STRING_IN_REGEXP, s2, r).negate();
 
@@ -984,12 +984,12 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
   if (index == 0)
   {
     s1 = nm->mkNode(STRING_SUBSTR, s, zero, b1);
-    s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+    s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(SUB, lens, b1));
   }
   else
   {
-    s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(MINUS, lens, b1), b1);
-    s2 = nm->mkNode(STRING_SUBSTR, s, zero, nm->mkNode(MINUS, lens, b1));
+    s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(SUB, lens, b1), b1);
+    s2 = nm->mkNode(STRING_SUBSTR, s, zero, nm->mkNode(SUB, lens, b1));
   }
   Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[index]).negate();
   std::vector<Node> nvec;
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index bbe25b7a3..3068c6815 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1989,8 +1989,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         else
         {
           // strip up to ( str.len(node[0]) - end_pt ) off the end of the string
-          curr =
-              d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
+          curr = d_arithEntail.rewrite(nm->mkNode(kind::SUB, tot_len, end_pt));
         }
       }
     }
@@ -2031,8 +2030,8 @@ Node SequencesRewriter::rewriteSubstr(Node node)
 
       // the length of a string from the inner substr subtracts the start point
       // of the outer substr
-      Node len_from_inner = d_arithEntail.rewrite(
-          nm->mkNode(kind::MINUS, node[0][2], start_outer));
+      Node len_from_inner =
+          d_arithEntail.rewrite(nm->mkNode(kind::SUB, node[0][2], start_outer));
       Node len_from_outer = node[2];
       Node new_len;
       // take quantity that is for sure smaller than the other
@@ -2136,7 +2135,7 @@ Node SequencesRewriter::rewriteUpdate(Node node)
   {
     // str.update(str.rev(s), n, t) --->
     //   str.rev(str.update(s, len(s) - (n + 1), t))
-    Node idx = nm->mkNode(MINUS,
+    Node idx = nm->mkNode(SUB,
                           nm->mkNode(STRING_LENGTH, s),
                           nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1))));
     Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s[0], idx, x));
@@ -2579,7 +2578,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
 
   Node len0 = nm->mkNode(STRING_LENGTH, node[0]);
   Node len1 = nm->mkNode(STRING_LENGTH, node[1]);
-  Node len0m2 = nm->mkNode(MINUS, len0, node[2]);
+  Node len0m2 = nm->mkNode(SUB, len0, node[2]);
 
   if (node[1].isConst())
   {
@@ -2669,7 +2668,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
           Node nn = utils::mkConcat(children0, stype);
           Node ret =
               nm->mkNode(PLUS,
-                         nm->mkNode(MINUS, node[2], new_len),
+                         nm->mkNode(SUB, node[2], new_len),
                          nm->mkNode(STRING_INDEXOF, nn, node[1], new_len));
           return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
         }
@@ -3035,8 +3034,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
           kind::STRING_SUBSTR,
           lastChild1[0],
           lastChild1[1],
-          nm->mkNode(
-              kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1))));
+          nm->mkNode(kind::PLUS, len0, one, nm->mkNode(kind::NEG, partLen1))));
       Node res = nm->mkNode(kind::STRING_REPLACE,
                             node[0],
                             utils::mkConcat(children1, stype),
@@ -3551,7 +3549,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   }
   else
   {
-    val = NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens);
+    val = NodeManager::currentNM()->mkNode(kind::SUB, lent, lens);
   }
 
   // Check if we can turn the prefix/suffix into equalities by showing that the
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 03c9f9375..a92fd3424 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -211,7 +211,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
     id = SK_PREFIX;
     b = nm->mkNode(
-        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
+        SUB, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
   }
   else if (id == SK_ID_VC_SPT)
   {
@@ -224,7 +224,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
     id = SK_PREFIX;
     b = nm->mkNode(
-        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1)));
+        SUB, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1)));
   }
   else if (id == SK_ID_DC_SPT)
   {
@@ -264,9 +264,9 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
     Node la = nm->mkNode(STRING_LENGTH, a);
     Node lb = nm->mkNode(STRING_LENGTH, b);
-    Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
+    Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(SUB, la, lb))
                     : utils::mkSuffix(a, lb);
-    Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
+    Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(SUB, lb, la))
                     : utils::mkSuffix(b, la);
     id = SK_PURIFY;
     // SK_ID_V_UNIFIED_SPT(x,y) --->
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 952a1a36b..7491f510f 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -146,13 +146,13 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
           Node s = n1[sindex_use];
           size_t slen = Word::getLength(s);
           Node ncl = nm->mkConstInt(cvc5::Rational(slen));
-          Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
+          Node next_s = nm->mkNode(SUB, lowerBound, ncl);
           next_s = d_rr->rewrite(next_s);
           Assert(next_s.isConst());
           // we can remove the entire constant
           if (next_s.getConst<Rational>().sgn() >= 0)
           {
-            curr = d_rr->rewrite(nm->mkNode(MINUS, curr, ncl));
+            curr = d_rr->rewrite(nm->mkNode(SUB, curr, ncl));
             success = true;
             sindex++;
           }
@@ -162,7 +162,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
             // lower bound minus the length of a concrete string is negative,
             // hence lowerBound cannot be larger than long max
             Assert(lbr < Rational(String::maxSize()));
-            curr = d_rr->rewrite(nm->mkNode(MINUS, curr, lowerBound));
+            curr = d_rr->rewrite(nm->mkNode(SUB, curr, lowerBound));
             uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
             Assert(lbsize < slen);
             if (dir == 1)
@@ -190,7 +190,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
     else
     {
       Node next_s = NodeManager::currentNM()->mkNode(
-          MINUS,
+          SUB,
           curr,
           NodeManager::currentNM()->mkNode(STRING_LENGTH, n1[sindex_use]));
       next_s = d_rr->rewrite(next_s);
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 4c2319b4e..2667c1989 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -85,7 +85,7 @@ Node StringsPreprocess::reduce(Node t,
     // len(s) - n -m
     Node b13 = nm->mkNode(
         OR,
-        nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))),
+        nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(PLUS, n, m))),
         nm->mkNode(EQUAL, lsk2, zero));
     // Length of the result is at most m
     Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
@@ -139,7 +139,7 @@ Node StringsPreprocess::reduce(Node t,
     }
     else
     {
-      rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(MINUS, lens, n));
+      rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(SUB, lens, n));
     }
     Node rslen = nm->mkNode(STRING_LENGTH, rs);
     Node nsuf = nm->mkNode(PLUS, n, rslen);
@@ -187,10 +187,8 @@ Node StringsPreprocess::reduce(Node t,
     Node negone = nm->mkConstInt(Rational(-1));
 
     // substr( x, n, len( x ) - n )
-    Node st = nm->mkNode(STRING_SUBSTR,
-                         x,
-                         n,
-                         nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
+    Node st = nm->mkNode(
+        STRING_SUBSTR, x, n, nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), n));
     Node io2 =
         sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
     Node io4 =
@@ -216,17 +214,16 @@ Node StringsPreprocess::reduce(Node t,
     Node c31 = st.eqNode(nm->mkNode(STRING_CONCAT, io2, y, io4));
     // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
     Node c32 =
-        nm->mkNode(
-              STRING_CONTAINS,
-              nm->mkNode(
-                  STRING_CONCAT,
-                  io2,
-                  nm->mkNode(
-                      STRING_SUBSTR,
-                      y,
-                      zero,
-                      nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))),
-              y)
+        nm->mkNode(STRING_CONTAINS,
+                   nm->mkNode(
+                       STRING_CONCAT,
+                       io2,
+                       nm->mkNode(
+                           STRING_SUBSTR,
+                           y,
+                           zero,
+                           nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, y), one))),
+                   y)
             .negate();
     // skk = n + len( io2 )
     Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2)));
@@ -281,7 +278,7 @@ Node StringsPreprocess::reduce(Node t,
                        nm->mkNode(GEQ, i, n),
                        nm->mkNode(LT, i, nm->mkNode(ITE, retNegOne, sLen, skk)),
                        nm->mkNode(GT, l, zero),
-                       nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, i)),
+                       nm->mkNode(LEQ, l, nm->mkNode(SUB, sLen, i)),
                    });
     Node body = nm->mkNode(
         OR,
@@ -293,10 +290,9 @@ Node StringsPreprocess::reduce(Node t,
     //     ~in_re(substr(s, i, l), r)
     Node firstMatch = utils::mkForallInternal(bvl, body);
     Node bvll = nm->mkNode(BOUND_VAR_LIST, l);
-    Node validLen =
-        nm->mkNode(AND,
-                   nm->mkNode(GEQ, l, zero),
-                   nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, skk)));
+    Node validLen = nm->mkNode(AND,
+                               nm->mkNode(GEQ, l, zero),
+                               nm->mkNode(LEQ, l, nm->mkNode(SUB, sLen, skk)));
     Node matchBody = nm->mkNode(
         AND,
         validLen,
@@ -362,7 +358,7 @@ Node StringsPreprocess::reduce(Node t,
     Node ux = nm->mkNode(APPLY_UF, u, x);
     Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
     Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
-    Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
+    Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0);
 
     Node ten = nm->mkConstInt(Rational(10));
     Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
@@ -428,7 +424,7 @@ Node StringsPreprocess::reduce(Node t,
     Node kc2 = nm->mkNode(LT, k, lens);
     Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
     Node codeSk = nm->mkNode(
-        MINUS,
+        SUB,
         nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
         c0);
     Node ten = nm->mkConstInt(Rational(10));
@@ -458,7 +454,7 @@ Node StringsPreprocess::reduce(Node t,
     Node sx = nm->mkNode(STRING_SUBSTR, s, x, one);
     Node ux = nm->mkNode(APPLY_UF, u, x);
     Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one));
-    Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
+    Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0);
 
     Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
     Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten));
@@ -518,7 +514,7 @@ Node StringsPreprocess::reduce(Node t,
     // length of first skolem is second argument
     Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
     Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
-    Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, t12));
+    Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12));
     Node b1 = nm->mkNode(AND, b11, b12, b13);
 
     // nodes for the case where `seq.nth` is undefined.
@@ -571,7 +567,7 @@ Node StringsPreprocess::reduce(Node t,
                        nm->mkNode(kind::STRING_SUBSTR,
                                   y,
                                   zero,
-                                  nm->mkNode(kind::MINUS,
+                                  nm->mkNode(kind::SUB,
                                              nm->mkNode(kind::STRING_LENGTH, y),
                                              one))),
                    y)
@@ -634,11 +630,11 @@ Node StringsPreprocess::reduce(Node t,
     Node ufi = nm->mkNode(APPLY_UF, uf, i);
     Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one));
     Node ii = nm->mkNode(STRING_INDEXOF, x, y, ufi);
-    Node cc = nm->mkNode(
-        STRING_CONCAT,
-        nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)),
-        z,
-        nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
+    Node cc =
+        nm->mkNode(STRING_CONCAT,
+                   nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi)),
+                   z,
+                   nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
 
     std::vector<Node> flem;
     flem.push_back(ii.eqNode(negOne).negate());
@@ -782,7 +778,7 @@ Node StringsPreprocess::reduce(Node t,
     Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1);
     Node ulip1 = nm->mkNode(APPLY_UF, ul, ip1);
     // ii = Uf(i + 1) - Ul(i + 1)
-    Node ii = nm->mkNode(MINUS, ufip1, ulip1);
+    Node ii = nm->mkNode(SUB, ufip1, ulip1);
 
     std::vector<Node> flem;
     // Ul(i + 1) > 0
@@ -805,8 +801,7 @@ Node StringsPreprocess::reduce(Node t,
     // forall l. 0 < l < Ul(i + 1) =>
     //   ~in_re(substr(x, Uf(i + 1) - Ul(i + 1), l), y')
     flem.push_back(utils::mkForallInternal(bvll, shortestMatchBody));
-    Node pfxMatch =
-        nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi));
+    Node pfxMatch = nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi));
     // Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
     flem.push_back(
         nm->mkNode(APPLY_UF, us, i)
@@ -907,8 +902,8 @@ Node StringsPreprocess::reduce(Node t,
     Node i = SkolemCache::mkIndexVar(t);
     Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
 
-    Node revi = nm->mkNode(
-        MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
+    Node revi =
+        nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
     Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one);
     Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one);
 
@@ -941,7 +936,7 @@ Node StringsPreprocess::reduce(Node t,
         NodeManager::currentNM()->mkNode(
             kind::LEQ,
             b1,
-            NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)),
+            NodeManager::currentNM()->mkNode(kind::SUB, lenx, lens)),
         NodeManager::currentNM()->mkNode(
             kind::EQUAL,
             NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index abac46d37..a65f98e7e 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -150,7 +150,7 @@ Node mkSuffix(Node t, Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
   return nm->mkNode(
-      STRING_SUBSTR, t, n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, t), n));
+      STRING_SUBSTR, t, n, nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, t), n));
 }
 
 Node getConstantComponent(Node t)
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 71ce2d3e8..623a38c81 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -401,8 +401,8 @@ TEST_F(TestNodeBlackNode, getKind)
   n = d_nodeManager->mkNode(PLUS, x, y);
   ASSERT_EQ(PLUS, n.getKind());
 
-  n = d_nodeManager->mkNode(UMINUS, x);
-  ASSERT_EQ(UMINUS, n.getKind());
+  n = d_nodeManager->mkNode(NEG, x);
+  ASSERT_EQ(NEG, n.getKind());
 }
 
 TEST_F(TestNodeBlackNode, getOperator)
@@ -513,7 +513,7 @@ TEST_F(TestNodeBlackNode, kinded_iterator)
   Node y = d_skolemManager->mkDummySkolem("y", integerType);
   Node z = d_skolemManager->mkDummySkolem("z", integerType);
   Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
-  Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
+  Node x_minus_y = d_nodeManager->mkNode(kind::SUB, x, y);
 
   {  // iterator
     Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index 779397e04..d9be92249 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -313,7 +313,7 @@ TEST_F(TestNodeBlackNodeBuilder, append)
   Node p = d_nodeManager->mkNode(
       EQUAL,
       d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0),
-      d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
+      d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(NEG, s), t));
   Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
 
 #ifdef CVC5_ASSERTIONS
diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp
index 9127fadff..989651aee 100644
--- a/test/unit/theory/arith_poly_white.cpp
+++ b/test/unit/theory/arith_poly_white.cpp
@@ -79,16 +79,16 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int)
   t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x});
   ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
 
-  t1 = d_nodeManager->mkNode(MINUS, t1, t2);
+  t1 = d_nodeManager->mkNode(SUB, t1, t2);
   t2 = zero;
   ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
 
-  t1 = d_nodeManager->mkNode(UMINUS, d_nodeManager->mkNode(PLUS, x, y));
-  t2 = d_nodeManager->mkNode(MINUS, zero, d_nodeManager->mkNode(PLUS, y, x));
+  t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(PLUS, x, y));
+  t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(PLUS, y, x));
   ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
 
-  t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, x), y);
-  t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, y), x);
+  t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, x), y);
+  t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, y), x);
   ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2));
 
   t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(PLUS, y, z));
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 8ce982291..71f6c240c 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -196,7 +196,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption)
   // x + 5 < 6 |= 0 > x --> false
   ASSERT_TRUE(!ae.checkWithAssumption(x_plus_five_lt_six, zero, x, true));
 
-  Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x);
+  Node neg_x = d_nodeManager->mkNode(kind::NEG, x);
   Node x_plus_five_lt_five =
       d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five));
 
diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp
index 3fcd74356..b3746db15 100644
--- a/test/unit/theory/theory_arith_rewriter_black.cpp
+++ b/test/unit/theory/theory_arith_rewriter_black.cpp
@@ -58,7 +58,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber)
   {
     RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 3);
     Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
-    n = d_nodeManager->mkNode(Kind::MINUS, n, n);
+    n = d_nodeManager->mkNode(Kind::SUB, n, n);
     n = d_slvEngine->getRewriter()->rewrite(n);
     EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
     EXPECT_EQ(n.getConst<Rational>(), Rational(0));
@@ -68,8 +68,8 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber)
     RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
     Node m = d_nodeManager->mkRealAlgebraicNumber(msqrt2);
     Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
-    Node mm = d_nodeManager->mkNode(Kind::UMINUS, m);
-    Node mn = d_nodeManager->mkNode(Kind::UMINUS, n);
+    Node mm = d_nodeManager->mkNode(Kind::NEG, m);
+    Node mn = d_nodeManager->mkNode(Kind::NEG, n);
     mm = d_slvEngine->getRewriter()->rewrite(mm);
     mn = d_slvEngine->getRewriter()->rewrite(mn);
     EXPECT_EQ(-msqrt2, sqrt2);