Method test_ratval_construction

tests/test_z3_ported.py:578–583

Guide: Q(1, 3) creates 1/3.

(self)

        assert prove(claim)

    def test_ratval_construction(self):
        """Guide: Q(1, 3) creates 1/3."""
        r = Q(1, 3)
        assert is_real(r)
        assert isinstance(r._ast, BinOpNode)
        assert r._ast.op == BinOp.DIV

    def test_ratval_structure(self):
        """Q(a, b) creates a/b as division."""