Method test_constant_array

tests/test_z3_ported.py:949–954

K(IntSort(), 0) creates an array where every element is 0.

(self, kernel)

        assert prove(claim)

    def test_constant_array(self, kernel):
        """K(IntSort(), 0) creates an array where every element is 0."""
        c = K(IntSort(), IntVal(0))
        i = Int("i")
        claim = ForAll([i], Select(c, i) == IntVal(0))
        assert prove(claim)

    def test_array_getitem_syntax(self):
        """a[i] is shorthand for Select(a, i)."""