func (ctx *Context) FloatNaN(s Sort) Float {
	val := Float(wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fpa_nan(ctx.c, s.c)
	}))
	runtime.KeepAlive(ctx)
	runtime.KeepAlive(s)
	return val
}
FloatNaN returns a floating-point NaN of sort s.
package z3
import (
	"math/big"
	"runtime"
)
import "C"
type Float value
func init() {
	kindWrappers[KindFloatingPoint] = func(x value) Value {
		return Float(x)
	}
}
func (ctx *Context) FloatSort(ebits, sbits int) Sort {
	var sort Sort
	ctx.do(func() {
		sort = wrapSort(ctx, C.Z3_mk_fpa_sort(ctx.c, C.uint(ebits), C.uint(sbits)), KindFloatingPoint)
	})
	return sort
}
type RoundingMode int
const (
	RoundToNearestEven RoundingMode = iota
	RoundToNearestAway
	RoundToPositive
	RoundToNegative
	RoundToZero
	roundingModesNum
)
var roundingModeKey = &[]string{"z3.roundingModeKey"}[0]
func (rm RoundingMode) ast(ctx *Context) value {
	cache, _ := ctx.Extra(roundingModeKey).([]value)
	if cache == nil {
		cache = make([]value, roundingModesNum)
		cache[RoundToNearestEven] = wrapValue(ctx, func() C.Z3_ast {
			return C.Z3_mk_fpa_rne(ctx.c)
		})
		cache[RoundToNearestAway] = wrapValue(ctx, func() C.Z3_ast {
			return C.Z3_mk_fpa_rna(ctx.c)
		})
		cache[RoundToPositive] = wrapValue(ctx, func() C.Z3_ast {
			return C.Z3_mk_fpa_rtp(ctx.c)
		})
		cache[RoundToNegative] = wrapValue(ctx, func() C.Z3_ast {
			return C.Z3_mk_fpa_rtn(ctx.c)
		})
		cache[RoundToZero] = wrapValue(ctx, func() C.Z3_ast {
			return C.Z3_mk_fpa_rtz(ctx.c)
		})
		ctx.SetExtra(roundingModeKey, cache)
	}
	return cache[rm]
}
func (ctx *Context) rm() value {
	ctx.lock.Lock()
	rm := ctx.roundingModeAST
	ctx.lock.Unlock()
	if rm.valueImpl == nil {
		rm = ctx.roundingMode.ast(ctx)
		ctx.lock.Lock()
		ctx.roundingModeAST = rm
		ctx.lock.Unlock()
	}
	return rm
}
func (ctx *Context) SetRoundingMode(rm RoundingMode) RoundingMode {
	rmv := rm.ast(ctx)
	ctx.lock.Lock()
	old := ctx.roundingMode
	ctx.roundingMode = rm
	ctx.roundingModeAST = rmv
	ctx.lock.Unlock()
	return old
}
func (ctx *Context) RoundingMode() RoundingMode {
	ctx.lock.Lock()
	defer ctx.lock.Unlock()
	return ctx.roundingMode
}