From 1e6c7645d3d98ba734ab73ed76c7785b572b86c8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 13 Dec 2021 13:48:49 -0600
Subject: Initial cut at distinguishing uses of CONST_RATIONAL (#7682)

---
 src/theory/strings/eager_solver.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/theory/strings/eager_solver.cpp')

diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp
index ac8e815df..0e5c19658 100644
--- a/src/theory/strings/eager_solver.cpp
+++ b/src/theory/strings/eager_solver.cpp
@@ -227,7 +227,7 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
   Assert(e != nullptr);
   Assert(!t.isNull());
   Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
-  Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL)
+  Assert(!tb.isNull() && tb.isConst() && tb.getType().isInteger())
       << "Unexpected bound " << tb << " from " << t;
   Rational br = tb.getConst<Rational>();
   Node prev = isLower ? e->d_firstBound : e->d_secondBound;
@@ -236,7 +236,7 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
   {
     // convert to bound
     Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower);
-    Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL);
+    Assert(!prevb.isNull() && prevb.isConst() && prevb.getType().isInteger());
     Rational prevbr = prevb.getConst<Rational>();
     if (prevbr == br || (br < prevbr) == isLower)
     {
@@ -251,7 +251,8 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
   {
     // are we in conflict?
     Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower);
-    Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL);
+    Assert(!prevob.isNull() && prevob.isConst()
+           && prevob.getType().isInteger());
     Rational prevobr = prevob.getConst<Rational>();
     if (prevobr != br && (prevobr < br) == isLower)
     {
-- 
cgit v1.2.3