Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)

This changes the `STRINGS_ARRAY_UPDATE_BOUND` inference to explicitly
include the disequality between the term before and after the update if
the update has an effect. This is an optimization that prevents us from
splitting on that (dis-)equality later on.

diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp
index e31a5e5a4c1ca6a16c9f6a4abdb811c2049eaff7..4be5ec04da8d2dd2103821d93ab479cb8eebb40e 100644 (file)
--- a/src/theory/strings/array_core_solver.cpp
+++ b/src/theory/strings/array_core_solver.cpp
@@ -145,14 +145,15 @@ void ArrayCoreSolver::checkUpdate(const std::vector<Node>& updateTerms)
                          false,
                          true);
 
-      // update(s, n, t)
+      // x = update(s, n, t)
       // ------------------------
-      // 0 <= n < len(t) and nth(s, n) != nth(update(s, n, t)) ||
-      // s = update(s, n, t)
+      // 0 <= n < len(t) and nth(s, n) != nth(update(s, n, t))  and x != s ||
+      // x = s
       lem = nm->mkNode(
           OR,
           nm->mkNode(AND,
                      left.eqNode(nm->mkNode(SEQ_NTH, n[0], n[1])).notNode(),
+                     n.eqNode(n[0]).negate(),
                      cond),
           n.eqNode(n[0]));
       d_im.sendInference(