(self, idx: ArithRef | int)
| 3893 | ) |
| 3894 | |
| 3895 | def __getitem__(self, idx: ArithRef | int) -> ExprRef: |
| 3896 | if isinstance(idx, int): |
| 3897 | idx = IntVal(idx) |
| 3898 | sort = self._sort |
| 3899 | elem_sort = sort._elem if isinstance(sort, SeqSortRef) else IntSort() |
| 3900 | return ExprRef( |
| 3901 | SeqNthNode(self._ast, idx._ast), |
| 3902 | elem_sort, |
| 3903 | _merge(self._vars, idx._vars), |
| 3904 | ) |
| 3905 | |
| 3906 | def at(self, idx: ArithRef | int) -> ExprRef: |
| 3907 | """Return a unit sequence at the given index.""" |
nothing calls this directly
no test coverage detected