В процессе поиска ответов на свои вопросы про cvc5 наткнулся на конспект по солверам. Это большой сборник примеров. Очень легко читается (и он на рунглише), местами написана чушь, но он неплох для погружения в область, если кому интересна эта тема. От души разбавлено байками.

Среди интересного можно увидеть ломание генератора случайных чисел, решение задачки из комикса xkcd, доказательство корректности всяких битовых хаков, факторизацию числа, решение задачи расцветки графа, чтобы занимать меньше регистров памяти, поиск коллизий в CRC32, минимизацию количества тестов.