Method test_ite_construction

tests/test_z3_ported.py:1054–1057

(self)

    """From z3py guide: If(cond, then, else)."""

    def test_ite_construction(self):
        x = Int("x")
        expr = If(x > 0, x, -x)
        assert isinstance(expr._ast, IteNode)

    def test_ite_type_preservation(self):
        """If returns same sort as branches."""