Method test_set_union

tests/test_z3_compat.py:2000–2006

SetUnion creates an array expression.

(self)

        assert _try_prove(claim)

    def test_set_union(self):
        """SetUnion creates an array expression."""

        a = SetAdd(EmptySet(IntSort()), IntVal(1))
        b = SetAdd(EmptySet(IntSort()), IntVal(2))
        u = SetUnion(a, b)
        assert isinstance(u, ExprRef)

    def test_set_intersect(self):
        """SetIntersect creates an array expression."""