Method test_bv_and_self

tests/test_z3_ported.py:679–683

x & x == x.

(self, kernel)

        assert prove(claim)

    def test_bv_and_self(self, kernel):
        """x & x == x."""
        x = BitVec("x", 8)
        claim = ForAll([x], (x & x) == x)
        assert prove(claim)

    def test_bv_or_self(self, kernel):
        """x | x == x."""