--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on November 2013 ---
I should add that I'm getting similar results (mostly unproved goals) for *really* trivial examples like below. Curiously, for each goal either all solvers rapidly prove it or else all solvers timeout. I suspect I just installed something incorrectly but I don't know how to debug it. John #include <stdint.h> /*@ requires (r > 0) && (r < 32) */ uint32_t rotate_left (uint32_t x, uint32_t r) { return (x << r) | (x >> (32-r)); }