func (lit Real) AsRat() (numer, denom Int, isLiteralRational bool) {
	if lit.astKind() != C.Z3_NUMERAL_AST {
		return Int{}, Int{}, false
	}
	numer = Int(wrapValue(lit.ctx, func() C.Z3_ast {
		return C.Z3_get_numerator(lit.ctx.c, lit.c)
	}))
	denom = Int(wrapValue(lit.ctx, func() C.Z3_ast {
		return C.Z3_get_denominator(lit.ctx.c, lit.c)
	}))
	runtime.KeepAlive(lit)
	return numer, denom, true
}
AsRat returns the value of lit as a numerator and denominator Int
literals. If lit is not a literal or is not rational, it returns
false for isLiteralRational. To round an arbitrary real to be
rational, see method Real.Approx.
package z3
import (
	"math/big"
	"runtime"
	"unsafe"
)
import "C"
type Real value
func init() {
	kindWrappers[KindReal] = func(x value) Value {
		return Real(x)
	}
}
func (ctx *Context) RealSort() Sort {
	var sort Sort
	ctx.do(func() {
		sort = wrapSort(ctx, C.Z3_mk_real_sort(ctx.c), KindReal)
	})
	return sort
}
func (ctx *Context) RealConst(name string) Real {
	return ctx.Const(name, ctx.RealSort()).(Real)
}
func (ctx *Context) FromBigRat(val *big.Rat) Real {
	cstr := C.CString(val.String())
	defer C.free(unsafe.Pointer(cstr))
	sort := ctx.RealSort()
	sval := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_numeral(ctx.c, cstr, sort.c)
	})
	runtime.KeepAlive(sort)
	return Real(sval)
}