Simple byte array in Z3 (SMT)

Question

I try make a simple example for checking bytes in fixed array. I read also Z3 tutorials but i can't get it working. Here is may scenario:

I have fixed byte array with length of 16: T(16)

I have these conditions to check:

A = (T(16) + 1) And 0x0F
T(A) = 0x76
0x01 <= A <= 0x7F

It mean take byte from T(16) add 1, make AND with 0x0F, and assign result number to variable A. Now check if in array T on position A T(A) is number 0x76. Also A can be between values 0x01 and 0x7F.

These conditions are repeating for more positions in array, but I need get it working just for first case. The goal of this is: find right order of known bytes in fixed array based on given equations.

I try it with this script but doesn't work.

Error: operator is applied to arguments of the wrong sort.

(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)

Example:

on T(16) is value 0x14, + 1 = 0x15, AND 0x0F = 0x05, on T(0x05) should be value 0x76.

Thank you.

usr usr · Accepted Answer · 2015-09-28T09:15:13

You can't mix integers and bitvectors like that and there is no need. Use bitvectors of size 8 in all cases. Don't use Int.

Besides that this will work.

You might find that not using arrays but only bitvectors is faster. This is something to experiment with.

Simple byte array in Z3 (SMT)

1 Answers