Method test_store_select_ground

tests/test_z3_compat.py:1811–1817

Store(a, i, v)[i] == v.

(self, kernel)

    """Array operations proven through Lean."""

    def test_store_select_ground(self, kernel):
        """Store(a, i, v)[i] == v."""
        a = Array("a", IntSort(), IntSort())
        i = Int("i")
        v = Int("v")
        claim = Select(Store(a, i, v), i) == v
        assert _try_prove(claim)

    def test_store_select_different_index(self, kernel):
        """Store(a, i, v)[j] == a[j] when i != j."""