Разобрался с примерчиком про деление. Вкратце - как и ожидалось, просто ошибка в генерации промежуточного кода из-за которой не сходятся типы: Напомню исходное: typedef int32_t my_int; my_int ref (my_int n) { return n/2; } my_int imp (my_int n) { return n>>1; } Увы: вместо искомого, скрипт выдает: clang -emit-llvm -c div2.c -o div2.bc saw div2_llvm.saw [05:06:40.821] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/div2_llvm.saw" [05:06:40.824] Extracting reference term: ref [05:06:40.841] Extracting implementation term: imp [05:06:40.844] Proving equivalence: ref == imp [05:06:40.869] Cryptol error: [error] at /home/msk/WORK/SNOB/SAW/sl-basic/c/div2_llvm.saw:11:30--11:33: Type mismatch: Expected type: 33 Inferred type: 32 ../Makefile.common:9: recipe for target 'saw_c' failed Замечу, что если заменить тип на int16_t, то оно вполне корректно ругается... Написал скриптик, который печатает типы подгруженных функций и их деревяшки: l <- llvm_load_module "div2.bc"; print "Extracting reference term: ref"; ref <- crucible_llvm_extract l "ref"; print_type ref; print_term ref; print ""; print "Extracting implementation term: imp"; imp <- crucible_llvm_extract l "imp"; print_type imp; print_term imp; Как и ожидалось: [09:31:09.379] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/d2.saw" [09:31:09.403] Extracting reference term: ref [09:31:09.413] (arg_0 : Prelude.bitvector 0x20) -> Prelude.Vec 0x21 Prelude.Bool [09:31:09.414] \(arg_0 : Prelude.bitvector 0x20) -> Prelude.bvSDiv 0x20 arg_0 (Prelude.bvNat 0x20 0x2) [09:31:09.415] [09:31:09.416] Extracting implementation term: imp [09:31:09.420] (arg_0 : Prelude.bitvector 0x20) -> Prelude.Vec 0x20 Prelude.Bool [09:31:09.421] \(arg_0 : Prelude.bitvector 0x20) -> Prelude.bvSShr 0x1f arg_0 0x1 Причина - видимо по каким-то причинам в библиотеке ихней знаковое деление имеет тип с разрядностью на 1 больше аргументов. Для сложения-вычитания это даже и необходимо, зачем может понадобиться для деления - не очень понимаю. В 16-ти же битном варианте генерируется более страхолюдный код с приведением к 32-битному и вырезанию 167 бит из результата обратно (просто потому что в С так положено): [09:34:40.702] \(arg_0 : Prelude.bitvector 0x10) -> Prelude.slice Prelude.Bool 0x10 0x10 0x0 (Prelude.bvSDiv 0x20 (Prelude.bvSExt 0x10 0xf arg_0) (Prelude.bvNat 0x20 0x2)) который естественно имеет правльный тип: [09:34:40.701] (arg_0 : Prelude.bitvector 0x10) -> Prelude.Vec 0x10 Prelude.Bool Upd: Если кому-то интересно - исходный код тут: https://github.com/kouzdra/public-files-/blob/master/SAW/div2.c https://github.com/kouzdra/public-files-/blob/master/SAW/div2_16.c ASTs: https://github.com/kouzdra/public-files-/blob/master/SAW/div2.saw_tree https://github.com/kouzdra/public-files-/blob/master/SAW/div2_16.saw_tree Upd: была бага - засабмитил - (говорят) пофиксили.