a[i] is shorthand for Select(a, i).
(self)
| 954 | assert prove(claim) |
| 955 | |
| 956 | def test_array_getitem_syntax(self): |
| 957 | """a[i] is shorthand for Select(a, i).""" |
| 958 | a = Array("a", IntSort(), IntSort()) |
| 959 | i = Int("i") |
| 960 | sel = a[i] |
| 961 | assert isinstance(sel._ast, SelectNode) |
| 962 | |
| 963 | def test_lambda_array(self): |
| 964 | """Lambda as array comprehension.""" |