From f36f21fa8c64c30c8a775ae6ca4950674bda33ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2023 13:36:41 -0800
Subject: [PATCH] add comments for API versions of bit-vector
 overflow/underflow checks for #7011

---
 src/api/api_bv.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp
index bb4263730..3ea5ba918 100644
--- a/src/api/api_bv.cpp
+++ b/src/api/api_bv.cpp
@@ -227,6 +227,9 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
     Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         RESET_ERROR_CODE();
+        // l1 := t1 <s 0
+        // l2 := t2 <s 0
+        // l1 & l2 => t1 + t2 <s 0
         Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
         Z3_inc_ref(c, zero);
         Z3_ast r = Z3_mk_bvadd(c, t1, t2);
@@ -255,6 +258,10 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
     Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         RESET_ERROR_CODE();
+        // x := t2 = min_int
+        // y := t1 <s 0
+        // z := no_overflow(t1 + -t2)
+        // if x y z
         Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
         Z3_inc_ref(c, minus_t2);
         Z3_sort s = Z3_get_sort(c, t2);
@@ -284,6 +291,9 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_TRY;
         RESET_ERROR_CODE();
         if (is_signed) {
+            // x := 0 <s -t2
+            // y := no_underflow(x + -t2)
+            // x => y
             Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
             Z3_inc_ref(c, zero);
             Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);