func (ctx *Context) Interrupt() {
	C.Z3_interrupt(ctx.c)
	runtime.KeepAlive(ctx)
}
Interrupt stops the current solver, simplifier, or tactic being
executed by ctx.
package z3
import (
	"fmt"
	"runtime"
	"sync"
	"unsafe"
)
import "C"
type Context struct {
	*contextImpl
	syms map[string]C.Z3_symbol
	roundingMode RoundingMode
	roundingModeAST value
	extra map[interface{}]interface{}
	lock sync.Mutex
}
type contextImpl struct {
	c C.Z3_context
}
func goZ3ErrorHandler(ctx C.Z3_context, e C.Z3_error_code) {
	msg := C.Z3_get_error_msg_ex(ctx, e)
	panic(C.GoString(msg))
}
func NewContext(config *Config) *Context {
	cfg := C.Z3_mk_config()
	defer C.Z3_del_config(cfg)
	if config != nil {
		for key, val := range config.m {
			ckey, cval := C.CString(key), C.CString(fmt.Sprint(val))
			defer C.free(unsafe.Pointer(ckey))
			defer C.free(unsafe.Pointer(cval))
			C.Z3_set_param_value(cfg, ckey, cval)
		}
	}
	impl := &contextImpl{C.Z3_mk_context_rc(cfg)}
	runtime.SetFinalizer(impl, func(impl *contextImpl) {
		C.Z3_del_context(impl.c)
	})
	ctx := &Context{
		impl,
		make(map[string]C.Z3_symbol),
		RoundToNearestEven,
		value{},
		nil,
		sync.Mutex{},
	}
	C.Z3_set_error_handler(ctx.c, (*C.Z3_error_handler)(C.goZ3ErrorHandler))
	return ctx
}
func NewContextConfig() *Config {
	return newConfig([]param{
		{"timeout", "uint", "Timeout in milliseconds used for solvers"},
		{"rlimit", "uint", "Resource limit used for solvers"},
		{"well_sorted_check", "bool", "Type checker"},
		{"auto_config", "bool", "Use heuristics to automatically select solver and configure it"},
		{"model_validate", "bool", "Validate models produced by solvers"},
		{"dump_models", "bool", "Dump models whenever check-sat returns sat"},
		{"trace", "bool", "Trace generation for VCC"},
		{"trace_file_name", "string", "Trace out file for VCC traces"},
		{"debug_ref_count", "bool", "Debug support for AST reference counting"},
		{"smtlib2_compliant", "bool", "Enable SMT-LIB 2.0 compliance"},
		{"proof", "bool", "Enable proof generation"},
		{"model", "bool", "Enable model generation for solvers"},
		{"unsat_core", "bool", "Enable unsat-core generation for solvers"},
	})
}
func (ctx *Context) Config() *Config {
	cfg := NewContextConfig()
	cfg.set = ctx.setParam
	return cfg
}
func (ctx *Context) setParam(name string, val interface{}) {
	cname, cval := C.CString(name), C.CString(fmt.Sprint(val))
	defer C.free(unsafe.Pointer(cname))
	defer C.free(unsafe.Pointer(cval))
	ctx.do(func() {
		C.Z3_update_param_value(ctx.c, cname, cval)
	})
}