Method test_toint

tests/test_z3_compat.py:978–982

(self)

        assert r.sort() == RealSort()

    def test_toint(self):
        x = Real("x")
        r = ToInt(x)
        assert isinstance(r._ast, ToIntNode)
        assert r.sort() == IntSort()

    def test_sum(self):
        x, y, z = Ints("x y z")