From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 26 Mar 2022 03:46:31 +0000 (-0500)
Subject: Fix spurious assertion failure (#8404)
X-Git-Tag: cvc5-1.0.0~159
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d49f537e5bc394d9b6e6728c1875062aa2b1e39c;p=cvc5.git

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 df10f47a4..1d821e62b 100644
--- 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 097aa5e32..f7a26e535 100644
--- 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
index 000000000..9d6bb61b6
--- /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)))))