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 のはずですが、7 です)
sat
((s "74g\x00!!#2#$$")
(someBitVec10 #b0000000111))
z3 の bv2intやint2bvが失敗する簡単な例を教えてください。ありがとう！