func (l BV) Xnor(r BV) BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvxnor(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return BV(val)
}
Xnor returns the bit-wise xnor of l and r.

l and r must have the same size.
package z3
import "runtime"
import "C"
func (l BV) Eq(r BV) 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 BV) NE(r BV) Bool {
	return l.ctx.Distinct(l, r)
}
func (l BV) Not() BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvnot(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return BV(val)
}
func (l BV) AllBits() BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvredand(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return BV(val)
}
func (l BV) AnyBits() BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvredor(ctx.c, l.c)
	})
	runtime.KeepAlive(l)
	return BV(val)
}
func (l BV) And(r BV) BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvand(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return BV(val)
}
func (l BV) Or(r BV) BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvor(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return BV(val)
}
func (l BV) Xor(r BV) BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvxor(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return BV(val)
}
func (l BV) Nand(r BV) BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvnand(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return BV(val)
}
func (l BV) Nor(r BV) BV {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_bvnor(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return BV(val)
}