Fix pydoc doctest failures by updating expected output format for string operations

[Copilot]

The pyodide pipeline was failing due to doctest mismatches in the Z3 Python API. The issue was that Z3's string representation for sequence extraction operations changed from Extract(...) format to str.substr(...) format, but the docstring examples still expected the old format.

Changes made:

• Extract function: Updated expected output from Extract(StringVal("hello"), 1, 3) to str.substr("hello", 1, 3)
• SubString function: Updated expected output from Extract(StringVal("hello world"), 6, 5) to str.substr("hello world", 6, 5)
• SubSeq function: Updated expected output from Extract(StringVal("hello world"), 0, 5) to str.substr("hello world", 0, 5)

Example of the fix:

>>> s = StringVal("hello")
>>> Extract(s, 1, 3)  # Extract 3 characters starting at position 1
str.substr("hello", 1, 3)  # Updated from: Extract(StringVal("hello"), 1, 3)

These changes align the documentation with Z3's current output format and resolve the build failures in the pyodide pipeline.

Fixes #7702.

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.