[00:29:37] <vasil.s.d> Всем привет! Кто-нибудь может помочь мне координатами, кроме report@adacore.com, куда можно слать ошибки, найденные в gnatprove/why3 модулях?
С report@adacore.com перестали отвечать (по поводу последней ошибки относительно зависания gprbuild - тишина, хотя до этого отвечали по поводу других ошибок довольно оперативно) :(
А сейчас нашёл проблему при верификации SPARK кода (верификация инстанциирования generic модуля для modular 54,55,58,59 бит нормально,а вот 56 и 57 бит - не может доказать одно свойство), причём, это проблема либо драйверов why3 в SAT/SMT, либо gnatprove -> why3 (возможно, проблемы с теориями для битовых векторов - пока подробно не разбирался) и не знаю куда по этому поводу обращаться.