Method test_select_store_same_index

tests/test_z3_compat.py:599–606

Store then Select at the same index gives the written value.

(self, kernel)

        assert isinstance(c._ast, ConstArrayNode)

    def test_select_store_same_index(self, kernel):
        """Store then Select at the same index gives the written value."""
        a = Array("a", IntSort(), IntSort())
        v = Int("v")
        written = Store(a, IntVal(3), v)
        read_back = Select(written, IntVal(3))
        claim = ForAll([a, v], read_back == v)
        assert _try_prove(claim)

    def test_constant_array_read(self, kernel):
        """Reading from a constant array gives the constant value."""