diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
| commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
| tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /src/theory/strings/eager_solver.cpp | |
| parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
| parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) | |
Merge branch 'master' into cav22-stringscav22-strings
Diffstat (limited to 'src/theory/strings/eager_solver.cpp')
| -rw-r--r-- | src/theory/strings/eager_solver.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
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) { |