Method test_realval_integer

tests/test_z3_semantic.py:455–456

(self, kernel)

        assert _try_prove(-Q(1, 3) + Q(1, 3) == Q(0, 1))

    def test_realval_integer(self, kernel):
        assert _try_prove(RealVal(5) == ToReal(IntVal(5)))

    def test_realval_float_half(self, kernel):
        """0.5 as a Real should equal 1/2."""