Method test_tuple_constructor

tests/test_z3_ported.py:3354–3358

(self, kernel)

        assert Pair.name() == "Pair_t1"

    def test_tuple_constructor(self, kernel):
        Pair, mk_pair, [fst, snd] = TupleSort("Pair_t2", [IntSort(), IntSort()])
        assert isinstance(mk_pair, FuncDeclRef)
        assert mk_pair.arity() == 2
        assert mk_pair.name() == "Pair_t2"

    def test_tuple_accessors(self, kernel):
        Pair, mk_pair, [fst, snd] = TupleSort("Pair_t3", [IntSort(), IntSort()])