Method test_bv_sub_self

tests/test_z3_ported.py:703–707

x - x == 0.

(self, kernel)

        assert prove(claim)

    def test_bv_sub_self(self, kernel):
        """x - x == 0."""
        x = BitVec("x", 8)
        claim = ForAll([x], x - x == BitVecVal(0, 8))
        assert prove(claim)

    def test_shift_left_right(self, kernel):
        """(x << 2) >> 2 masks top bits (logical shift)."""