Method test_tuple_constructor_call

tests/test_z3_ported.py:3367–3372

(self, kernel)

        assert snd.arity() == 1

    def test_tuple_constructor_call(self, kernel):
        Pair, mk_pair, [fst, snd] = TupleSort("Pair_t4", [IntSort(), RealSort()])
        x = Int("x")
        y = Real("y")
        p = mk_pair(x, y)
        assert isinstance(p, ExprRef)

    def test_triple_sort(self, kernel):
        Triple, mk, accs = TupleSort("Triple_t5", [IntSort(), RealSort(), BoolSort()])