Method test_bv_xor_self_is_zero

tests/test_z3_ported.py:673–677

x ^ x == 0.

(self, kernel)

        assert prove(claim)

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

    def test_bv_and_self(self, kernel):
        """x & x == x."""