ULT has SignExt simplification, ULE(Q) does not #7389
Description
Hello there,
I have noticed that ULE(a_bv32, SignExt(24, b_bv8)) does not get properly simplified, while ULT(a_bv32, SignExt(24, b_bv8)) is: see the code below. This is not specific to the bitsize of the operands in the example (32).
I may be mistaken, but I believe this simplification should be possible considering ULE(x, y) is equivalent to Or(ULT(x, y), x == y).
>>> simplify(ULT(BitVecVal(53, 32), SignExt(24, BitVec('x', 8))))
Not(And(Extract(7, 6, x) == 0,
Extract(7, 7, x) == 0,
ULE(Extract(5, 0, x), 53)))
>>> simplify(ULE(BitVecVal(53, 32), SignExt(24, BitVec('x', 8))))
ULE(53,
Concat(Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
Extract(7, 7, x),
x))As for versioning: I'm using the Python package z3-solver with version 4.13.0.0
Additional substantiation can be found in #7380.
This significantly impacts the performance of my application, so it would be great if this could be looked into. :-)