Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 18 Feb 2022 20:18:04 +0000 (12:18 -0800)
committerGitHub <noreply@github.com>
Fri, 18 Feb 2022 20:18:04 +0000 (20:18 +0000)
commit23df33f277f12e43df2c0b676578f90d53dba7bb
tree8c4e5caa49c1bc6e861d7a5f4b02ba8f1530c8e0
parentcdef52f07aef156ad19dea89862a1b8d4373ea3a
Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)

Our `STRINGS_ARRAY_NTH_UPDATE` inference was missing an explanation that
establishes the relation between the update and the nth term. On the
current set of benchmarks, this does not cause an issue, but there
should be cases where it does. The commit also changes the array core solver
to take better advantage of `d_indexMap`.
src/theory/strings/array_core_solver.cpp