Method test_forall_basic

tests/test_z3_ported.py:991–995

(self)

    """Ported from z3py guide & socrates.py."""

    def test_forall_basic(self):
        x = Int("x")
        q = ForAll([x], x + 0 == x)
        assert isinstance(q._ast, ForAllNode)
        assert is_quantifier(q)

    def test_exists_basic(self):
        x = Int("x")