(self, kernel)
| 3358 | assert mk_pair.name() == "Pair_t2" |
| 3359 | |
| 3360 | def test_tuple_accessors(self, kernel): |
| 3361 | Pair, mk_pair, [fst, snd] = TupleSort("Pair_t3", [IntSort(), IntSort()]) |
| 3362 | assert isinstance(fst, FuncDeclRef) |
| 3363 | assert isinstance(snd, FuncDeclRef) |
| 3364 | assert fst.arity() == 1 |
| 3365 | assert snd.arity() == 1 |
| 3366 | |
| 3367 | def test_tuple_constructor_call(self, kernel): |
| 3368 | Pair, mk_pair, [fst, snd] = TupleSort("Pair_t4", [IntSort(), RealSort()]) |