Ограничения решателей SMT

Традиционно большая часть работы с вычислительной логикой была либо пропозициональной, и в этом случае вы использовали SAT (решатель булевой выполнимости ), либо первый -порядок, и в этом случае вы использовали средство доказательства теорем первого -порядка.

В последние годы был достигнут большой прогресс в SMT (решателях выполнимости по модулю теории ), которые в основном дополняют логику высказываний теориями арифметики и т. д.; Джон Рашби из SRI International заходит так далеко, что называет их прорывной технологией.

Каковы наиболее важные практические примеры проблем, которые могут быть решены в логике первого порядка -, но все еще не могут быть решены с помощью SMT? В частности, какие проблемы возникают, которые не могут быть решены с помощью SMT в области проверки программного обеспечения?