Ограничения Klee (инструмент анализа программы LLVM)

http://klee.llvm.org/ - это работающий инструмент анализа программ. путем символьного выполнения и решения ограничений, поиска возможных входных данных, которые вызовут сбой программы, и вывода их в виде тестовых примеров. Это чрезвычайно впечатляющая разработка, которая до сих пор дала хорошие результаты, включая обнаружение ряда ошибок в наборе реализаций утилит Unix с открытым исходным кодом, которые считались одними из самых тщательно протестированных программ, когда-либо написанных

. ] Мой вопрос: что он не ?

Конечно, любой такой инструмент имеет естественный предел, заключающийся в том, что он не может читать мысли пользователя и угадывать, каким должен был быть результат. Но если не брать в расчет принципиально невозможное, большинство проектов, похоже, еще не используют Klee; каковы ограничения текущей версии, с какими ошибками и рабочими нагрузками она еще не справляется?