我尝试做一个简单的例子来检查固定数组中的字节。我还阅读了 Z3 教程，但我无法让它工作。这是可能的情况：
我有长度为 16 的固定字节数组：T(16(
我有以下条件要检查：
A = (T(16) + 1) And 0x0F
T(A) = 0x76
0x01 <= A <= 0x7F
这意味着从T(16)加1中获取字节，用0x0F进行AND，并将结果编号分配给变量A。现在检查在位置A T(A)的数组T中是否是数字0x76。此外，A可以在值 0x01 和 0x7F 之间。
这些条件在数组中的更多位置重复出现，但我需要让它只针对第一种情况工作。这样做的目标是：根据给定的方程找到固定数组中已知字节的正确顺序。
我尝试使用此脚本，但不起作用。
错误：运算符应用于错误排序的参数。
(declare-const t (Array Int Int))
(declare-const a Int)
; A = (t(16) + 1) And 0x0F
(assert (= a (bvand (+ (select t 16) 1) #x0F)))
; t(A) = 0x76
(assert (= (select t a) #x76))
(check-sat)
;(get-model)
例：
在T(16)上是值0x14，+ 1 = 0x15，AND 0x0F = 0x05，在T(0x05)上应该是值0x76。
谢谢。
你不能像那样混合整数和位向量，也没有必要。在所有情况下都使用大小为 8 的位向量。不要使用Int .
除此之外，这将起作用。
您可能会发现不使用数组而仅使用位向量会更快。这是值得尝试的东西。