Method test_is_quantifier

tests/test_z3_ported.py:1556–1560

(self)

        assert not is_const(x + 1)

    def test_is_quantifier(self):
        x = Int("x")
        assert is_quantifier(ForAll([x], x > 0))
        assert is_quantifier(Exists([x], x > 0))
        assert not is_quantifier(x > 0)

    def test_is_eq_ne(self):
        x, y = Ints("x y")