Method test_bv_add_zero

tests/test_z3_ported.py:697–701

x + 0 == x.

(self, kernel)

        assert prove(claim)

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

    def test_bv_sub_self(self, kernel):
        """x - x == 0."""