Раз уж форум немного расшевелился ) Что сейчас по smt-решателям, есть нормально допиленые инструменты? Допустим я хочу найти в бинарнике все вызовы функции, где аргумент не константа, есть шанс такое автоматизировать?