Simplification issue?

[xarkes]

Hello,

I have an issue with z3, or more precisely something I cannot understand. I am using it to simplify some expressions. However I found one that seems quite obvious to me, but for some reason z3 is not able to simplify it.

from z3 import BitVec, simplify
r15 = BitVec('r15', 64)
expr = (((r15 & 0xFFFFFFFF) & 0xFFFFFFFF) ^ (((r15 & 0xFFFFFFFF) ^ 0x80000001) & 0xFFFFFFFF))
print(simplify(expr))

If we take a quick glance at the expression, and we know that the result will be 32 bits because of all the masks applied on every computation, the expression is the same as r15d ^ r15d ^ 0x80000001 (with r15d being the lowest 32bits value of r15), so it should be simplified to the following constant: 0x80000001, right?

So that's what I was expecting, z3 saying that the result of the simplification is a constant, however z3 yields some other expression, like this:

Concat(0, Extract(31, 0, r15)) ^
Concat(0,
       ~Extract(31, 31, r15),
       Extract(30, 1, r15),
       ~Extract(0, 0, r15))

If the result is not obvious, you can try to use any input as the value of r15, it will always be that constant, no matter what.

So I don't really understand why z3 fails to simplify this, and I hope someone can help me clarify this.
Thanks a lot :)

[xarkes]

So I guess that concat distribution was a missing feature then!
Thank you very much, I just tried on master and it seems to work like a charm!

[NikolajBjorner]

It seemed reasonable to include this rewrite. Already done for negation.