From 973123aa8dab1edf386b234f8b7b214a16965b23 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 29 Oct 2025 23:51:59 +0000
Subject: [PATCH] Improve documentation for Z3_OP_FINITE_SET_EXT and
 Z3_OP_FINITE_SET_MAP_INVERSE

- Clarified that Z3_OP_FINITE_SET_EXT returns a witness element demonstrating
  two sets are different (extensionality)
- Clarified that Z3_OP_FINITE_SET_MAP_INVERSE relates to pre-image reasoning

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/z3_api.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index fd570059f..d2a41e27e 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1002,9 +1002,9 @@ typedef enum
 
    - Z3_OP_FINITE_SET_RANGE: Range operation for finite sets of integers.
 
-   - Z3_OP_FINITE_SET_EXT: Finite set extensionality.
+   - Z3_OP_FINITE_SET_EXT: Finite set extensionality. Returns a witness element that is in one set but not the other, demonstrating that two sets are different.
 
-   - Z3_OP_FINITE_SET_MAP_INVERSE: Inverse of a finite set map operation.
+   - Z3_OP_FINITE_SET_MAP_INVERSE: Inverse image under a finite set map operation. Related to reasoning about the pre-image of elements under set mappings.
 
    - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
         information is exposed. Tools may use the string representation of the