Dafny handling bit vectors

• I'm trying to use Dafny with (unsigned) bitvectors (following this post).
• The following simplified example (permalink) works fine, but when I change to bv32, I get:
  • Unexpected prover response: timeout
• Is it a bug? or an expected performance gap between the two?
• Here is the code to make this post self contained:

method bitvectors()
{
    var a : bv16 := 0;
    // var a : bv32 := 0;
    ghost var atag := a;
    while (a<0xFFFF)
    // while (a<0xFFFFFFFF)
        invariant atag < 0xFFFF
        //invariant atag < 0xFFFFFFFF
    {
        atag := a;
        a := a+1;
    }
}

I'm hoping someone else has a better answer... but basically this is why I stay away from bitvectors :)

I did a little bit of digging, and it seems that on this particular example Dafny gets stuck in the termination check for the loop. At the Boogie level, comparing bitvectors involves converting them to mathematical integers, and then to real numbers, and then comparing those. It's pretty common for solvers to have trouble with these conversion functions, because they cut across different theories.

Sorry I couldn't be more helpful.