From f8ba42c5c4a2ea8eb5ce3cdc57230a92f964de47 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 18 Jun 2026 19:24:44 +0000
Subject: [PATCH] Clarify BV SMT2 regression assertion

---
 src/test/api.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/test/api.cpp b/src/test/api.cpp
index 8de8d8c06..b1765fdd4 100644
--- a/src/test/api.cpp
+++ b/src/test/api.cpp
@@ -99,6 +99,7 @@ void test_bvneg() {
         Z3_solver_push(ctx, s);
         Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, sx, minus_one));
         std::string smt2 = Z3_solver_to_string(ctx, s);
+        // Bit-vector numerals must print in canonical unsigned SMT2 form.
         ENSURE(smt2.find("(_ bv-") == std::string::npos);
         Z3_solver_pop(ctx, s, 1);
     }