func (l Real) Mul(r ...Real) Real {
	ctx := l.ctx
	cargs := make([]C.Z3_ast, len(r)+1)
	cargs[0] = l.c
	for i, arg := range r {
		cargs[i+1] = arg.c
	}
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_mul(ctx.c, C.uint(len(cargs)), &cargs[0])
	})
	runtime.KeepAlive(&cargs[0])
	return Real(val)
}
Mul returns the product l * r[0] * r[1] * ...
package z3
import "runtime"
import "C"
func (l Real) Eq(r Real) Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_eq(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Bool(val)
}
func (l Real) NE(r Real) Bool {
	return l.ctx.Distinct(l, r)
}
func (l Real) Div(r Real) Real {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_div(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Real(val)
}
func (l Real) ToInt() Int {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_real2int(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return Int(val)
}
func (l Real) IsInt() Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_is_int(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return Bool(val)
}
func (l Real) ToFloat(s Sort) Float {
	ctx := l.ctx
	rm := ctx.rm()
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_to_fp_real(ctx.c, rm.c, l.c, s.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(s)
	return Float(val)
}
func (l Real) ToFloatExp(exp Int, s Sort) Float {
	ctx := l.ctx
	rm := ctx.rm()
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_to_fp_int_real(ctx.c, rm.c, exp.c, l.c, s.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(exp)
	runtime.KeepAlive(s)
	return Float(val)
}
func (l Real) Add(r ...Real) Real {
	ctx := l.ctx
	cargs := make([]C.Z3_ast, len(r)+1)
	cargs[0] = l.c
	for i, arg := range r {
		cargs[i+1] = arg.c
	}
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_add(ctx.c, C.uint(len(cargs)), &cargs[0])
	})
	runtime.KeepAlive(&cargs[0])
	return Real(val)
}