diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 08a001c41970..e652f148081b 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -669,23 +669,38 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 | [] => 0#0
 | b :: bs => concat (ofBoolListLE bs) b
 
-/-- Overflow predicate for 2's complement unary minus -/
+/-- Overflow predicate for 2's complement unary minus.
+
+  SMT-Lib name: `bvnego`.
+-/
 
 def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1))
 
-/-- Overflow predicate for unsigned addition modulo 2^m -/
+/-- Overflow predicate for unsigned addition modulo 2^m.
+
+  SMT-Lib name: `bvuaddo`.
+-/
 
 def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w
 
-/-- Overflow predicate for signed addition on m-bit 2's complement -/
+/-- Overflow predicate for signed addition on m-bit 2's complement.
+
+  SMT-Lib name: `bvsaddo`.
+-/
 
 def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1))
 
-/-- Overflow predicate for unsigned multiplication modulo 2^m -/
+/-- Overflow predicate for unsigned multiplication modulo 2^m.
+
+  SMT-Lib name: `bvumulo`.
+-/
 
 def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w
 
-/-- Overflow predicate for signed multiplication on m-bit 2's complement -/
+/-- Overflow predicate for signed multiplication on m-bit 2's complement.
+
+  SMT-Lib name: `bvsmulo`.
+-/
 
 def smul_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1))