Читал страницу
https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях
там написано
«SMT включает также теории массивов и списков (часто используемые для моделирования и верификации программ)»
Ничего не понял. Расскажите, пожалуйста про теорию массивов.