z3 从位向量转换为整数

Question

有几篇关于位向量转换的帖子 到 z3 中的整数（反之亦然）。参见例如here， here 和 here。

documentation 表示 Z3_mk_bv2int 未被解释：

"...此函数本质上被视为未解释。 所以你不能指望 Z3 准确地反映这个的语义 使用此函数求解约束时的函数..."

但是，我找不到一个简单的例子它确实失败了 以反映预期的语义。 例如，每当我使用这样的查询时：

(declare-const s String)
(declare-const someBitVec10 (_ BitVec 10))

(assert (= s "74g\x00!!#2#$$"))

(assert (str.in.re (str.at s (bv2int someBitVec10)) (re.range "1" "3")))

(check-sat)
(get-value (s someBitVec10))

我得到了一个正确的答案（索引应该是 7，它是）

sat
((s "74g\x00!!#2#$$")
 (someBitVec10 #b0000000111))

谁能提供一个简单的例子，其中 z3 的 bv2int 和/或 int2bv 失败？？谢谢！

Answer 1

这个问题现在已经解决了，因为事实证明 int2bv 和 bv2int 确实是解释的。文档尚未更新，这可能会导致混乱（至少在我的情况下是这样）。所有细节都在this GitHub/z3/issues post。