Method mkReal

src/api/java/Context.java:2703–2710

Create a real from a fraction. @param num numerator of rational. @param den denominator of rational. @return A Term with value num/den and sort Real @see #mkNumeral(String v, R ty)

(int num, int den)

     * @see #mkNumeral(String v, R ty)
     **/
    public RatNum mkReal(int num, int den)
    {
        if (den == 0) {
            throw new Z3Exception("Denominator is zero");
        }

        return new RatNum(this, Native.mkReal(nCtx(), num, den));
    }

    /**
     * Create a real numeral.