title: Dafny handling bit vectors
body: <ul>
  <li>I'm trying to use Dafny with (unsigned) bitvectors (following <a href="https://stackoverflow.com/questions/63915841/dafny-modeling-integer-overflow">this post</a>).</li>
  <li>The following simplified example (<a href="https://rise4fun.com/Dafny/uGcst" rel="nofollow noreferrer">permalink</a>) works fine, but when I change to <code>bv32</code>, I get:
  <ul>
  <li><code>Unexpected prover response: timeout</code></li>
  </ul>
  </li>
  <li>Is it a bug? or an expected performance gap between the two?</li>
  <li>Here is the code to make this post self contained:</li>
  </ul>
  <pre><code>method bitvectors()
  {
      var a : bv16 := 0;
      // var a : bv32 := 0;
      ghost var atag := a;
      while (a&lt;0xFFFF)
      // while (a&lt;0xFFFFFFFF)
          invariant atag &lt; 0xFFFF
          //invariant atag &lt; 0xFFFFFFFF
      {
          atag := a;
          a := a+1;
      }
  }
  </code></pre>