From 2b8615f4fc2a9ad5cce2d2e48f163d8cca8789bc Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 1 Mar 2026 01:51:27 +0000
Subject: [PATCH] Add 8 missing BV overflow/underflow check functions to Go
 bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/go/bitvec.go | 48 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/src/api/go/bitvec.go b/src/api/go/bitvec.go
index 9ffd220ac..e98596160 100644
--- a/src/api/go/bitvec.go
+++ b/src/api/go/bitvec.go
@@ -158,3 +158,51 @@ func (c *Context) MkSignExt(i uint, expr *Expr) *Expr {
 func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr))
 }
+
+// MkBVAddNoOverflow creates a predicate that checks that the bit-wise addition
+// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
+func (c *Context) MkBVAddNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
+	return newExpr(c, C.Z3_mk_bvadd_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
+}
+
+// MkBVAddNoUnderflow creates a predicate that checks that the bit-wise signed addition
+// of t1 and t2 does not underflow.
+func (c *Context) MkBVAddNoUnderflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvadd_no_underflow(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVSubNoOverflow creates a predicate that checks that the bit-wise signed subtraction
+// of t1 and t2 does not overflow.
+func (c *Context) MkBVSubNoOverflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsub_no_overflow(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVSubNoUnderflow creates a predicate that checks that the bit-wise subtraction
+// of t1 and t2 does not underflow. If isSigned is true, checks for signed underflow.
+func (c *Context) MkBVSubNoUnderflow(t1, t2 *Expr, isSigned bool) *Expr {
+	return newExpr(c, C.Z3_mk_bvsub_no_underflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
+}
+
+// MkBVSdivNoOverflow creates a predicate that checks that the bit-wise signed division
+// of t1 and t2 does not overflow.
+func (c *Context) MkBVSdivNoOverflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsdiv_no_overflow(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVNegNoOverflow creates a predicate that checks that bit-wise negation does not overflow
+// when t1 is interpreted as a signed bit-vector.
+func (c *Context) MkBVNegNoOverflow(t1 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvneg_no_overflow(c.ptr, t1.ptr))
+}
+
+// MkBVMulNoOverflow creates a predicate that checks that the bit-wise multiplication
+// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
+func (c *Context) MkBVMulNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
+	return newExpr(c, C.Z3_mk_bvmul_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
+}
+
+// MkBVMulNoUnderflow creates a predicate that checks that the bit-wise signed multiplication
+// of t1 and t2 does not underflow.
+func (c *Context) MkBVMulNoUnderflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvmul_no_underflow(c.ptr, t1.ptr, t2.ptr))
+}