Fix unfolding logic of bv_simplify
bv_simplify
should always produce equalities on Z
, but due to a bug it turned bv_wrap n (bv_unsigned b) = bv_wrap n (bv_unsigned b)
into b = b
, which means that bv_solve
fails on bv_wrap n (bv_unsigned b) = bv_wrap n (bv_unsigned b)
. This MR fixes this bug which is caused by apply
applying an ↔
lemma in the wrong direction.