Method test_nat_induction_base

tests/test_z3_semantic.py:1409–1411

Base case of a simple property: 0 + 0 = 0.

(self, kernel)

        assert _try_prove(And(enc >= IntVal(0), enc <= IntVal(1)))

    def test_nat_induction_base(self, kernel):
        """Base case of a simple property: 0 + 0 = 0."""
        assert _try_prove(NatVal(0) + NatVal(0) == NatVal(0))

    def test_power_of_two_bv(self, kernel):
        """2^4 = 16 in 8-bit bitvectors."""