Z3 BitVector错误？

Question

Z3的位向量理论似乎存在一个缺陷。在ML接口中使用Expr.mk_numeral_string创建位向量常量，然后使用BitVector.get_string或BitVector.get_int读取表达式会导致不匹配。

以下是详细信息：

let create_bv_const ctx bv_str width = let bv_sort = BitVector.mk_sort ctx width in Expr.mk_numeral_string ctx bv_str bv_sort

现在

let bv1 = create_bv_const ctx "1111" 4.

使用Expr.to_string读取bv1会返回"7“，而它应该是"15”。

使用Expr.to_int时也会出现类似的错误。如果

let bv1 = create_bv_const ctx "0010" 4

读取bv1应该返回"2“，但Z3返回"10”。"0011“给出了"11”，而它应该是"3“。我尝试了宽度为5，8位的向量，也有类似的问题。但是对于width <=3位向量，它工作得很好。

我尝试了一个旧版本的Z3 (V4)，那里也有类似的问题。

我想创建包含位向量变量和常量的公式，并读出位向量值。

谢谢

Answer 1

1111mod 16 = 7，所以这是正确的。请注意，参数1111被读取为十进制数，而不是二进制数。