В общем - разобрался я "что это было и как это называется" (© Леонид Соболев). На деле оказалось не просто "тупо и просто", а "очень тупо и просто" - и довольно коряво, но для своего реального назначения вероятно самое то. На деле SAW при всей своей интересности жестко заточена под ровно одну задачу: верификацию криптографии, причем в основном той криптографии которую они пишут на Криптоле. А одна из главных фишек криптола (при всем его хаскелеобразии) - это возможность трансляции его кода в FPGA (ну или просто в жесткую логику). Разумеется - не любого кода, но вполне понятного подмножества: где ширины битовых полей ограничены, циклы по ним тоже невелики, а прочее делается "в потоке данных" (кой поток изображают свертки-зипперы с бесконечной рекурсией). Насколько этого достаточно на все криптографические случаи жизни, я сказать не возьмусь, но понятно что довольно многое туда попадает. Потому подход там очень простой: он тупо пытается раскрывать итерации и рекурсию путем "псевдоисполнения" просто даже не утруждая себя вопросами остановки. Если что - просто зацикливается. Если получилось - все хорошо, если нет - зациклится (приведенный мной пример с делением - просто ошибка в процессе развертки). Заодно понял и как оно казавшиеся головоломными примеры из того поста доказывает. Ну для простоты - на совсем элементарном примере: int fact( int n) { if (n == 0) return 1; return fact (m, n-1); } int fact6 () { return fact (6); } Если попробовать загрузить функцию fact, saw немедленно зациклится. А вот если fact6: m <- llvm_load_module "funcs.bc"; fact6 <- crucible_llvm_extract m "fact6"; print_term fact6; Все рабоает - только результат скучноват: [15:32:45.440][15:44:02.099] Loading file "/home/msk/WORK/SNOB/MISC/public-files-/SAW/funcs.saw" [15:44:02.141] Prelude.bvNat 32 1 Оно просто все посчитало. Чтобы не посчитало (поскольку в содержательных случаях такого обычно не бывает) - ну я просто параметр добавил: int fact_mul( int m, int n) { if (n == 0) return 1; return m * fact_mul (m, n-1); } int fact6_mul ( int m) { return fact_mul (m, 6); } Тут результат вплоне содержательный: [15:44:02.099] Loading file "/home/msk/WORK/SNOB/MISC/public-files-/SAW/funcs.saw" [15:44:02.141] \(arg_0 : Prelude.bitvector 32) -> Prelude.bvNat 32 1 [15:44:02.150] \(arg_0 : Prelude.bitvector 32) -> Prelude.bvMul 32 (Prelude.bvMul 32 (Prelude.bvMul 32 (Prelude.bvMul 32 (Prelude.bvMul 32 arg_0 arg_0) arg_0) arg_0) arg_0) arg_0 Ну и замечу что интеллекта на сравнения весьма хитроподвывернутых выражений такого рода у saw уже как раз очень хватает (причем делает он это в том примере на порядки быстрее чем "перебором вариантов". Еще будет наверное короткий комментарий по поводу исходного теста Файлы с этим добром: funcs.c funcs.saw funcs.saw_tree Makefile