1 files changed, 18 insertions, 11 deletions

diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 45881e1bb..50e03bfa5 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -22,6 +22,8 @@
 #include "theory/rewriter.h"
 #include "util/rational.h"
 
+using namespace cvc5::kind;
+
 namespace cvc5 {
 namespace theory {
 namespace arith {
@@ -36,7 +38,7 @@ Node pow2(uint64_t k)
 {
   Assert(k >= 0);
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkConst<Rational>(intpow2(k));
+  return nm->mkConst(CONST_RATIONAL, Rational(intpow2(k)));
 }
 
 bool oneBitAnd(bool a, bool b) { return (a && b); }
@@ -58,9 +60,9 @@ Node intExtract(Node x, uint64_t i, uint64_t size)
 IAndUtils::IAndUtils()
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_zero = nm->mkConst(Rational(0));
-  d_one = nm->mkConst(Rational(1));
-  d_two = nm->mkConst(Rational(2));
+  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  d_two = nm->mkConst(CONST_RATIONAL, Rational(2));
 }
 
 Node IAndUtils::createITEFromTable(
@@ -78,7 +80,8 @@ Node IAndUtils::createITEFromTable(
   Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
   // start with the default, most common value.
   // this value is represented in the table by (-1, -1).
-  Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
+  Node ite =
+      nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(-1, -1))));
   for (uint64_t i = 0; i < num_of_values; i++)
   {
     for (uint64_t j = 0; j < num_of_values; j++)
@@ -91,10 +94,13 @@ Node IAndUtils::createITEFromTable(
       // append the current value to the ite.
       ite = nm->mkNode(
           kind::ITE,
-          nm->mkNode(kind::AND,
-                     nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
-                     nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
-          nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
+          nm->mkNode(
+              kind::AND,
+              nm->mkNode(
+                  kind::EQUAL, x, nm->mkConst(CONST_RATIONAL, Rational(i))),
+              nm->mkNode(
+                  kind::EQUAL, y, nm->mkConst(CONST_RATIONAL, Rational(j)))),
+          nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(i, j)))),
           ite);
     }
   }
@@ -133,7 +139,7 @@ Node IAndUtils::createSumNode(Node x,
   // number of elements in the sum expression
   uint64_t sumSize = bvsize / granularity;
   // initialize the sum
-  Node sumNode = nm->mkConst<Rational>(0);
+  Node sumNode = nm->mkConst(CONST_RATIONAL, Rational(0));
   // compute the table for the current granularity if needed
   if (d_bvandTable.find(granularity) == d_bvandTable.end())
   {
@@ -260,7 +266,8 @@ Node IAndUtils::twoToK(unsigned k) const
 {
   // could be faster
   NodeManager* nm = NodeManager::currentNM();
-  Node ret = nm->mkNode(kind::POW, d_two, nm->mkConst(Rational(k)));
+  Node ret =
+      nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k)));
   ret = Rewriter::rewrite(ret);
   return ret;
 }