Dear SMT-LIB community,
As you may know, some of the array logics defined at
https://smt-lib.org/logics-all.shtml
contain certain restriction on the array sort to disallow nested
(multi-dimensional) arrays.
Specifically, the logics AUFLIA, AUFLIRA, QF_ABV, QF_AUFBV, and
QF_AUFLIA have this restriction.
In recent years, we received multiple benchmark submissions to the
SMT-LIB benchmark library that encode problems over nested arrays
arrays. However, due to this restriction, the majority of these
benchmarks were not included in an SMT-LIB benchmark library release.
Some of these benchmarks were not caught by our checking process during
benchmark submission and are already included some of those in QF_ABV
and AUFLIA. The majority of newly submitted benchmarks, however, are
kept in a separate repository since they are considered "non-standard"
right now.
We SMT-LIB maintainers propose to lift this restriction
on all array logics to allow arbitrarily nested arrays. If I remember
correctly this restriction was set in place in the past to make it
easier on solver developers to support a certain array logic. However,
we believe the restriction should not be on the logic since this
prevents users to submit benchmarks that require nested arrays to the
SMT-LIB benchmark library. Solver developers are still free to choose
whether they want to support nested array or not and the SMT-COMP
organizers can decide whether they want to include such benchmarks in
the competition.
Please feel free to comment until end of June 2025. If there are no
objections we will lift this restriction in the above logics and we will
include the currently pending benchmarks in next year's SMT-LIB release.
Cheers,
Mathias (on behalf of the SMT-LIB maintainers)