Incorrect result when performing a specific equality comparison of a symbolic value

[dnivra]

Describe the bug.

claripy returns an incorrect result for a specific equality comparison of a symbolic value, leading to a trace desync when symbolically tracing a binary(files for reproducing issue included below). On some testing, I found that this commit is probably the issue: tracing works fine when using its parent commit.

Environment Information.

Running in virtual environment at /home/dnivra/.virtualenvs/angr-dev
Platform: linux-x86_64
Python version: 3.8.5 (default, Jan 27 2021, 15:41:15)
[GCC 9.3.0]
######## angr #########
Python found it in /home/dnivra/angr-dev/angr/angr
Pip version angr 9.0.gitrolling
Git info:
Current commit bc992b4af0a48c05282846ae9f3cdf8290c5032a from branch master
Checked out from remote origin: https://github.com/angr/angr
######## ailment #########
Python found it in /home/dnivra/angr-dev/ailment/ailment
Pip version ailment 9.0.gitrolling
Git info:
Current commit 7db31a7b29910384062c358fb06c3250de2cddbb from branch master
Checked out from remote origin: https://github.com/angr/ailment
######## cle #########
Python found it in /home/dnivra/angr-dev/cle/cle
Pip version cle 9.0.gitrolling
Git info:
Current commit 4a7e4f7a6f1151f5587bf8bfa919da0064bd2449 from branch master
Checked out from remote origin: https://github.com/angr/cle
######## pyvex #########
Python found it in /home/dnivra/angr-dev/pyvex/pyvex
Pip version pyvex 9.0.gitrolling
Git info:
Current commit 38af62047b8a7785feeee6b5f243ad1dbd7db1f6 from branch master
Checked out from remote origin: https://github.com/angr/pyvex
######## claripy #########
Python found it in /home/dnivra/angr-dev/claripy/claripy
Pip version claripy 9.0.gitrolling
Git info:
Current commit ebd1313 from branch master
Checked out from remote origin: https://github.com/angr/claripy
######## archinfo #########
Python found it in /home/dnivra/angr-dev/archinfo/archinfo
Pip version archinfo 9.0.gitrolling
Git info:
Current commit 437b194538ccb0bf118b4b674613b88832b0b342 from branch master
Checked out from remote origin: https://github.com/angr/archinfo
######## z3 #########
Python found it in /home/dnivra/.virtualenvs/angr-dev/lib/python3.8/site-packages/z3
Pip version z3-solver 4.8.9.0
Couldn't find git info
######## unicorn #########
Python found it in /home/dnivra/.virtualenvs/angr-dev/lib/python3.8/site-packages/unicorn
Pip version unicorn 1.0.2rc4
Couldn't find git info
######### Native Module Info ##########
angr: <CDLL '/home/dnivra/angr-dev/angr/angr/lib/angr_native.so', handle 3350170 at 0x7fc8fd9a0cd0>
unicorn: <CDLL '/home/dnivra/.virtualenvs/angr-dev/lib/python3.8/site-packages/unicorn/lib/libunicorn.so', handle 2a85bb0 at 0x7fc8fcd7ddc0>
pyvex: <cffi.api._make_ffi_library..FFILibrary object at 0x7fc8fd8d2760>
z3: <CDLL '/home/dnivra/.virtualenvs/angr-dev/lib/python3.8/site-packages/z3/lib/libz3.so', handle 2ce6320 at 0x7fc8fa3dfa30>

To Reproduce.

This ZIP file contains a script, binary and input file to reproduce this issue. The bug is triggered by this claripy IROP line in VEX engine when executing the first VEX statement of instruction 0x8048ab87 during the second execution of block 0x8048ab65 by the VEX engine. It takes a few mins to reach the specific execution of this block.