1 files changed, 5 insertions, 9 deletions
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index 9a510c6f5..6cf26d357 100644
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -201,14 +201,10 @@ Node NormalForm::constructConstantBagFromElements(
   }
   TypeNode elementType = t.getBagElementType();
   std::map<Node, Rational>::const_reverse_iterator it = elements.rbegin();
-  Node bag = nm->mkBag(elementType,
-                       it->first,
-                       nm->mkConst<Rational>(CONST_RATIONAL, it->second));
+  Node bag = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second));
   while (++it != elements.rend())
   {
-    Node n = nm->mkBag(elementType,
-                       it->first,
-                       nm->mkConst<Rational>(CONST_RATIONAL, it->second));
+    Node n = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second));
     bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag);
   }
   return bag;
@@ -261,10 +257,10 @@ Node NormalForm::evaluateBagCount(TNode n)
   NodeManager* nm = NodeManager::currentNM();
   if (it != elements.end())
   {
-    Node count = nm->mkConst(CONST_RATIONAL, it->second);
+    Node count = nm->mkConstInt(it->second);
     return count;
   }
-  return nm->mkConst(CONST_RATIONAL, Rational(0));
+  return nm->mkConstInt(Rational(0));
 }
 
 Node NormalForm::evaluateDuplicateRemoval(TNode n)
@@ -592,7 +588,7 @@ Node NormalForm::evaluateCard(TNode n)
   }
 
   NodeManager* nm = NodeManager::currentNM();
-  Node sumNode = nm->mkConst(CONST_RATIONAL, sum);
+  Node sumNode = nm->mkConstInt(sum);
   return sumNode;
 }