Guide: Select and Store operations.
(self)
| 925 | assert is_array(a) |
| 926 | |
| 927 | def test_select_store(self): |
| 928 | """Guide: Select and Store operations.""" |
| 929 | a = Array("a", IntSort(), IntSort()) |
| 930 | b = Store(a, IntVal(0), IntVal(42)) |
| 931 | v = Select(b, IntVal(0)) |
| 932 | assert isinstance(v, ExprRef) |
| 933 | |
| 934 | def test_store_select_axiom(self, kernel): |
| 935 | """Select(Store(a, i, v), i) == v (read-over-write same index).""" |