From 84a6e4d67241ab83bc38b731dec43269aa0fa328 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 27 Jun 2025 19:11:04 -0700
Subject: [PATCH] Fix pydoc doctest failures by updating expected output format
 for string operations (#7703)

* Initial plan

* Fix pydoc doctest failures by updating expected output format

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/python/z3/z3.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 41df1fe69..c8e1d30a0 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -4249,7 +4249,7 @@ def Extract(high, low, a):
     >>> # Sequence extraction examples  
     >>> s = StringVal("hello")
     >>> Extract(s, 1, 3)  # Extract 3 characters starting at position 1
-    Extract(StringVal("hello"), 1, 3)
+    str.substr("hello", 1, 3)
     >>> simplify(Extract(StringVal("abcd"), 2, 1))  # Extract 1 character at position 2
     "c"
     >>> simplify(Extract(StringVal("abcd"), 0, 2))  # Extract first 2 characters  
@@ -11215,7 +11215,7 @@ def SubString(s, offset, length):
     
     >>> s = StringVal("hello world") 
     >>> SubString(s, 6, 5)  # Extract "world"
-    Extract(StringVal("hello world"), 6, 5)
+    str.substr("hello world", 6, 5)
     >>> simplify(SubString(StringVal("hello"), 1, 3))
     "ell"
     """
@@ -11229,7 +11229,7 @@ def SubSeq(s, offset, length):
     
     >>> s = StringVal("hello world")
     >>> SubSeq(s, 0, 5)  # Extract "hello"  
-    Extract(StringVal("hello world"), 0, 5)
+    str.substr("hello world", 0, 5)
     >>> simplify(SubSeq(StringVal("testing"), 2, 4))
     "stin"
     """