У меня был хороший опыт использования STP для символического исполнения. STP был разработан именно для этой задачи. Кроме того, было несколько символических инструментов выполнения, которые успешно использовали STP для этой цели, поэтому есть основания полагать, что STP не сосет. Я определенно рекомендую STP другим в качестве варианта по умолчанию для такого рода экспериментов.
Однако я не пробовал другие системы, поэтому не знаю, как STP сравнивается с ними.
Лично я вижу STP в качестве базовой линии и выбора по умолчанию для такого рода приложений. Так что, если у вас есть время попробовать только один решатель, попробовать STP кажется вполне разумным выбором.
Если бы мне пришлось угадывать, я бы предположил, что арифметику битовых векторов важно поддерживать, потому что любой большой системный код будет иметь нетривиальный объем кода, который выполняет побитовые операции. Кроме того, я подозреваю, что некоторые системные коды могут полагаться на поведение беззнаковой арифметики для переноса по модулю 2 n , и если вы попытаетесь смоделировать его с помощью целых чисел, вы не получите правильную семантику C (потому что, как вы говорите, целые числа просто не верны для машинной арифметики), и, следовательно, если вы попытаетесь использовать решатель только для целых чисел, у вас могут возникнуть некоторые трудности. Однако у меня нет веских доказательств для любого из этих подозрений.
P.S. Z3 также может быть претендентом на добавление в ваш список для рассмотрения. (Вам действительно нужен ваш решатель с открытым исходным кодом, если он бесплатный? Я ожидаю, что символический инструмент выполнения будет использовать его только как черный ящик, без изменений.)