(Z3Py) Concat, quantifiers and bit-vectors

Question

Is it possible to make use of quantifiers with bit-vectors and concatenations? To illustrate, running the following code in the newest Z3:

a = BitVec('a', 8)
b = Concat(BitVec('b', 4), BitVec('c', 4))

prove(ForAll(a, Exists(b, a == b)))

produces the following error:

BitVecRef instance has no attribute '__len__'

I have tried adding a simple __len__ method in BitVecRef but further problems arose.

Without the Concat, the code works as expected. For example:

a = BitVec('a', 8)
b = BitVec('b', 8)

prove(ForAll(a, Exists(b, a == b)))

outputs the correct: proved

Answer 1

Your example defines the value b as shorthand for a concatenation. It gets passed as the bound variable to the quantifier Exists(b, a == b). Quantifiers expect a list of basic constants, such as a, b, c below, but not compound expressions, such as d. Below is a version of your puzzle that gets processed:

a = BitVec('a', 8)
b = BitVec('b', 4)
c = BitVec('c', 4)
d = Concat(b, c)

prove(ForAll(a, Exists(b, a == d)))