func (l Float) Div(r Float) Float {
	ctx := l.ctx
	rm := ctx.rm()
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_div(ctx.c, rm.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Float(val)
}
Div returns l/r.

Div uses the current rounding mode.
package z3
import "runtime"
import "C"
func (l Float) Eq(r Float) 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 Float) NE(r Float) Bool {
	return l.ctx.Distinct(l, r)
}
func (l Float) Abs() Float {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_abs(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return Float(val)
}
func (l Float) Neg() Float {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_neg(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return Float(val)
}
func (l Float) Add(r Float) Float {
	ctx := l.ctx
	rm := ctx.rm()
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_add(ctx.c, rm.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Float(val)
}
func (l Float) Sub(r Float) Float {
	ctx := l.ctx
	rm := ctx.rm()
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_sub(ctx.c, rm.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Float(val)
}
func (l Float) Mul(r Float) Float {
	ctx := l.ctx
	rm := ctx.rm()
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_mul(ctx.c, rm.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Float(val)
}