Инструмент SMT, поддерживающий фиксированную точку

Я предполагаю, что под фиксированной точкой вы имеете в виду решение запросов предложения Хорна. Существует множество инструментов, которые решают проблемы аналогичного характера, но, возможно, не в одном и том же формате. Инструмент Leon от Philippe Suter использует различные алгоритмы и может решать многие запросы корректности рекурсивных программ. Инструмент ARMC Андрея Рыбальченко также решает формулы Хорна с линейной вещественной арифметикой. Он также может устанавливать условия прекращения. Системы CLP с таблицами также должны быть приспособлены для решения запросов в формате, похожем на Z3 (оба используют формулы Хорна в качестве входного формата). Существует также множество решателей для проверки символьных моделей, которые можно использовать в зависимости от вашего контекста.