Dafny 处理位向量

Question

• 我正在尝试将 Dafny 与（无符号）位向量一起使用（遵循 this post）。
• 以下简化示例 (permalink) 工作正常，但当我更改为 bv32 时，我得到：
  • Unexpected prover response: timeout
• 这是一个错误吗？还是两者之间的预期性能差距？
• 这里是使这篇文章独立的代码：

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;
    }
}

Answer 1

我希望其他人有更好的答案...但基本上这就是我远离位向量的原因:)

我做了一些挖掘，似乎在这个特定的例子中，Dafny 卡在了循环的终止检查中。在 Boogie 级别，比较位向量涉及将它们转换为数学整数，然后转换为实数，然后将它们进行比较。求解器在使用这些转换函数时遇到问题是很常见的，因为它们跨越了不同的理论。

很抱歉，我无法提供更多帮助。