有几篇关于在 z3 中将位向量转换为整数（反之亦然）的帖子。例如，请参见此处、 此处和此处。
文档说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失败？谢谢！