Fix spurious assertion failure (#8404)

This was wrong when doing sequences of reals and a seq.nth merges with a seq.len.

Fixes cvc5/cvc5-projects#502.

diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp
index df10f47a45b7617a8ced07eaf802fbf41914308a..1d821e62bd8901320dc37da8ed49cfa73491c7c0 100644 (file)
--- a/src/theory/strings/eager_solver.cpp
+++ b/src/theory/strings/eager_solver.cpp
@@ -126,9 +126,11 @@ bool EagerSolver::checkForMergeConflict(Node a,
                                         EqcInfo* eb)
 {
   Assert(eb != nullptr && ea != nullptr);
-  Assert(a.getType() == b.getType())
+  Assert(a.getType().isComparableTo(b.getType()))
       << "bad types for merge " << a << ", " << b;
-  Assert(a.getType().isStringLike() || a.getType().isInteger());
+  // usages of isRealOrInt are only due to subtyping, where seq.nth for
+  // sequences of Real are merged to integer equivalence classes
+  Assert(a.getType().isStringLike() || a.getType().isRealOrInt());
   // check prefix, suffix
   for (size_t i = 0; i < 2; i++)
   {
@@ -228,7 +230,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.isConst() && tb.getType().isInteger())
+  Assert(!tb.isNull() && tb.isConst() && tb.getType().isRealOrInt())
       << "Unexpected bound " << tb << " from " << t;
   Rational br = tb.getConst<Rational>();
   Node prev = isLower ? e->d_firstBound : e->d_secondBound;
@@ -237,7 +239,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.isConst() && prevb.getType().isInteger());
+    Assert(!prevb.isNull() && prevb.isConst() && prevb.getType().isRealOrInt());
     Rational prevbr = prevb.getConst<Rational>();
     if (prevbr == br || (br < prevbr) == isLower)
     {
@@ -253,7 +255,7 @@ 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.isConst()
-           && prevob.getType().isInteger());
+           && prevob.getType().isRealOrInt());
     Rational prevobr = prevob.getConst<Rational>();
     if (prevobr != br && (prevobr < br) == isLower)
     {

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 097aa5e32d62f7b7f34d5cbf10fa969ff41735b8..f7a26e535a66f1c1833c5c00467a44abb7a4f373 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2562,6 +2562,7 @@ set(regress_1_tests
   regress1/strings/proj254-re-elim-agg.smt2
   regress1/strings/proj-issue281.smt2
   regress1/strings/proj-issue331.smt2
+  regress1/strings/proj-issue502-merge-type.smt2
   regress1/strings/query4674.smt2
   regress1/strings/query8485.smt2
   regress1/strings/re-all-char-hard.smt2

diff --git a/test/regress/cli/regress1/strings/proj-issue502-merge-type.smt2 b/test/regress/cli/regress1/strings/proj-issue502-merge-type.smt2
new file mode 100644 (file)
index 0000000..9d6bb61
--- /dev/null
+++ b/test/regress/cli/regress1/strings/proj-issue502-merge-type.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(check-sat-assuming ((seq.nth (seq.unit (is_int (seq.nth (seq.unit real.pi) 1))) (to_int (seq.nth (seq.unit real.pi) 1)))))