7 files changed, 15 insertions, 13 deletions
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
index df8fb9383..8dac2cfda 100644
--- a/test/unit/node/node_algorithm_black.cpp
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -140,8 +140,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
 {
   TypeNode integer = d_nodeManager->integerType();
 
-  Node one = d_nodeManager->mkConst(Rational(1));
-  Node two = d_nodeManager->mkConst(Rational(2));
+  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
 
   Node x = d_nodeManager->mkBoundVar(integer);
   Node a = d_skolemManager->mkDummySkolem("a", integer);
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index b170ccbb6..50e766e61 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -732,15 +732,15 @@ TEST_F(TestNodeBlackNode, isConst)
   Node cons_1_nil =
       d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
                             cons,
-                            d_nodeManager->mkConst(Rational(1)),
+                            d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
                             d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
   Node cons_1_cons_2_nil = d_nodeManager->mkNode(
       APPLY_CONSTRUCTOR,
       cons,
-      d_nodeManager->mkConst(Rational(1)),
+      d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
       d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
                             cons,
-                            d_nodeManager->mkConst(Rational(2)),
+                            d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)),
                             d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
   ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
   ASSERT_FALSE(cons_x_nil.isConst());
@@ -749,8 +749,8 @@ TEST_F(TestNodeBlackNode, isConst)
 
   TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                                 d_nodeManager->integerType());
-  Node zero = d_nodeManager->mkConst(Rational(0));
-  Node one = d_nodeManager->mkConst(Rational(1));
+  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
   Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
   ASSERT_TRUE(storeAll.isConst());
 
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index 05ccfc90c..779397e04 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -312,7 +312,7 @@ TEST_F(TestNodeBlackNodeBuilder, append)
 
   Node p = d_nodeManager->mkNode(
       EQUAL,
-      d_nodeManager->mkConst<Rational>(0),
+      d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0),
       d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
   Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
 
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index b02790cb5..ad41155c3 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -140,7 +140,7 @@ TEST_F(TestNodeBlackNodeManager, mkConst_bool)
 TEST_F(TestNodeBlackNodeManager, mkConst_rational)
 {
   Rational r("3/2");
-  Node n = d_nodeManager->mkConst(r);
+  Node n = d_nodeManager->mkConst(CONST_RATIONAL, r);
   ASSERT_EQ(n.getConst<Rational>(), r);
 }
 
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index fe06f85d3..64f6a70f5 100644
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -23,6 +23,7 @@
 namespace cvc5 {
 
 using namespace cvc5::expr;
+using namespace cvc5::kind;
 
 namespace test {
 
@@ -33,8 +34,8 @@ class TestNodeWhiteNodeManager : public TestNode
 TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
 {
   Rational i("3");
-  Node n = d_nodeManager->mkConst(i);
-  Node m = d_nodeManager->mkConst(i);
+  Node n = d_nodeManager->mkConst(CONST_RATIONAL, i);
+  Node m = d_nodeManager->mkConst(CONST_RATIONAL, i);
   ASSERT_EQ(n.getId(), m.getId());
 }
 
diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp
index eb6f77bdc..8061526d5 100644
--- a/test/unit/node/node_white.cpp
+++ b/test/unit/node/node_white.cpp
@@ -49,7 +49,7 @@ TEST_F(TestNodeWhiteNode, iterators)
   Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
   Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
   Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
-  Node two = d_nodeManager->mkConst(Rational(2));
+  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
   Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
 
   Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index 9f93017f0..424fee989 100644
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -50,7 +50,8 @@ TEST_F(TestNodeWhiteTypeNode, sub_types)
   TypeNode bvType = d_nodeManager->mkBitVectorType(32);
 
   Node x = d_nodeManager->mkBoundVar("x", realType);
-  Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
+  Node xPos = d_nodeManager->mkNode(
+      GT, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
   TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
   Node lambda = d_nodeManager->mkVar("lambda", funtype);
   std::vector<Node> formals;