I wrote this post for my students at Brown. I've gotten a bit better at using Copilot since then. But I also wanted to share it in public as an exercise in honesty. Here's what went well, and not so well, when I used Copilot for a maintenance task.

Picking up from my last post, I’d just used Copilot to very quickly build a native library. The experience was great, and I felt like I was part of a team: I could clarify and point out issues, Copilot could bring “expertise” I didn’t have.

Anger

After integrating the new library into the project, the program ran briefly but then crashed. A different library couldn’t be loaded. This wasn’t one we had modified! So what could be going on? I started a fresh conversation.

I’m not going the long, tangled chat log; in the end I had to start a new conversation. Some things went very well, like identifying the temporary folder where the libraries were being copied. But it was progressively more frustrating:

  • Copilot wanted to do irreversible things, like deleting files it didn’t need to delete.
  • Copilot wanted to hard-code paths from my laptop into the build, which would have broken the tool for anybody but me.
  • It would periodically declare everything solved, then spam me with a long list of comforting green check marks.
  • I am so. So. SO tired of:
    • “You’re absolutely right!” (I usually wasn’t.)
    • “Perfect!” (Even my typos.)
    • “That’s a brilliant insight!” (No.)
    • “Now I see the complete picture! (For the third time.)

LLM sycophancy isn’t going to make us spoiled toddlers. It’s going to make us angry. For real, I had to get up and take a walk to calm down after being told I was brilliant after nearly every query. I knew I was really just stumbling around in the dark. The praise turned bitter in my stomach and I went to bed angry.

Insight

I did some poking around on my own in the morning, and discovered an exception being thrown when Java was loading the library. I threw away the old conversation and started a new one that focused on this specific exception. (I’ve also included this new chat log in another appendix, edited for space.)

Here was the exception. I don’t expect you to read it, and I didn’t want to either. Help, Copilot!

java.lang.UnsatisfiedLinkError: /private/var/folders/5s/1rkxr1w132q1cm68mf5lghk40000gq/T/AMALGAMALPHA-tbn/binary/libz3java.dylib: dlopen(/private/var/folders/5s/1rkxr1w132q1cm68mf5lghk40000gq/T/AMALGAMALPHA-tbn/binary/libz3java.dylib, 0x0001): Library not loaded: libz3.dylib
  Referenced from: <34D2681D-AF03-38D8-BFF2-71CBDCA23B2C> 
/private/var/folders/5s/1rkxr1w132q1cm68mf5lghk40000gq/T/AMALGAMALPHA-tbn/binary/libz3java.dylib
  Reason: tried: 'libz3.dylib' (no such file),
 '/System/Volumes/Preboot/Cryptexes/OSlibz3.dylib' (no such file), 
'libz3.dylib' (no such file), 
'/usr/lib/libz3.dylib' (no such file, not in dyld cache), '/Users/tbn/repos/others/OldCompSAT/libz3.dylib' (no such file), 
'/System/Volumes/Preboot/Cryptexes/OS/Users/tbn/repos/others/OldCompSAT/libz3.dylib' (no such file), 
'/Users/tbn/repos/others/OldCompSAT/libz3.dylib' (no such file),
 '/usr/lib/libz3.dylib' (no such file, not in dyld cache)
Failed to load (C): libz3java.dylib

The library was being loaded, but one of its dependencies wasn’t. Copilot suggested some sort of Java version mismatch might be the cause, and pointed me to a JAR file that connected the native library and the actual project. So the chain was something like:

My application <- JAR file <- the library <- the dependency

I asked Copilot about the JAR file. As it was replying I realized: these universal libraries were built by combining two platform-specific libraries: one for x86 and one for arm64. What if Java wasn’t the versioning problem; could the native libraries be built from different versions of the original C++ code? Yes. In the end, there were multiple mismatches. * The JAR file was built for library version 4.3.2. * The x86 library was built from version 4.5.1.0. * The arm64 library was built from version 4.12.2.0.

Copilot didn’t find the exception by itself; I needed to do that. It also didn’t get to the root cause by itself, but the conversation led to me realizing the problem. Copilot “knew” a lot more than I did about how to work with these libraries. It was Copilot’s suggestions that gave me the information I needed to jump to the right conclusion. We were a team again.

That said, the full responses were so verbose—full of headers and sub-headers and emoji and exclamation points—that they were hard to get through. Maybe next time I’ll write an instructions file.

Copilot Log: The Second Library Problem

tnelson: The tool rooted here comprises two repositories, AmalgamKodkod and OldCompoSAT. The tool runs at least two distinct processes: the GUI and the worker. There is some engineering debt: the same code sometimes runs but on different processes. It was originally built for Java 8 (and this is the Java it is being run under now), on Intel macs. Sometimes when running, `/OldCompoSAT/src/edu/mit/csail/sdg/alloy4/WorkerEngine.java` the readObject() on line 196 returns a StreamCorruptedException. Hypothesize and diagnose, asking questions.

GitHub Copilot: I’ll help you diagnose the StreamCorruptedException in WorkerEngine.java. Let me start by examining the code and understanding the context of the error. Let me search for the WorkerEngine.java file in the workspace: The file path seems correct but it’s showing as duplicated. Let me check the actual file structure: Great! Now let me read the WorkerEngine.java file around line 196: Now let me see the main method and the worker process side of the communication: Now let me see the beginning of the file to understand the class structure and the wrap method: Let me see the rest of the wrap method and the process management code: Now let me also check if there are any related classes like WorkerTask implementations to understand what kind of objects are being serialized: Let me examine the SimpleReporter.java to understand what kinds of tasks are being serialized: Now let me search for any serialVersionUID issues or version-related problems: Let me also check if there are any issues with process communication or timing issues: Now let me check what happens around line 196 more carefully. The issue seems to be in the manager thread where readObject() is called: Based on my analysis of the code, I can now provide a comprehensive diagnosis of the StreamCorruptedException occurring at line 196 in WorkerEngine.java.

Diagnosis of StreamCorruptedException

The StreamCorruptedException occurs on line 196 where sub2main.readObject() is called. This is a classic inter-process communication issue in a multi-threaded environment. Here are the most likely causes and my hypotheses:

Primary Hypotheses:

  1. Process Termination Race Condition: The subprocess may be terminating unexpectedly while the parent process is trying to read from the ObjectInputStream. This creates a corrupted stream state.

  2. Stream Desynchronization: The ObjectOutputStream and ObjectInputStream can become desynchronized if:
    • The subprocess writes partial data before crashing
    • Multiple threads access the streams concurrently
    • The subprocess process exits between write operations

  3. Serialization Version Mismatch: I noticed that many classes use serialVersionUID = 0, which is problematic. If the same code runs in different processes (as you mentioned), but they were compiled at different times or with different versions, the serialization can fail.

  4. Memory/Resource Pressure: The subprocess might be running out of memory (especially on older Java 8 with limited heap) and crash while serializing objects, corrupting the stream.
Key Evidence from Code Analysis:
  • Line 196 is in a while(true) loop that continuously reads objects from the subprocess
  • The code uses process reuse: “the same subprocess is reused to execute each subsequent task”
  • There’s a complex synchronization mechanism with latest_sub and latest_manager
  • The subprocess is launched with specific memory constraints (-Xmx and -Xss parameters)
Diagnostic Questions:
  1. Timing Pattern: Does this exception occur:
    • Randomly during long-running operations?
    • Consistently after a certain number of successful operations?
    • More frequently under heavy load or memory pressure?

  2. Process State: When this happens, is the subprocess (latest_sub) still alive, or has it terminated?

  3. Memory Usage: Are you seeing any OutOfMemoryError or other memory-related issues in the subprocess before the StreamCorruptedException?

  4. Platform Specifics: You mentioned this runs on Intel Macs with Java 8 - are you seeing any JVM crash logs in the directory (like the hs_err_pid*.log files I noticed in the OldCompSAT directory)?

  5. Concurrent Operations: Are multiple tasks being submitted to the WorkerEngine simultaneously, or is this happening during sequential operations?
  1. Add logging around the readObject() call to capture the stream state
  2. Check subprocess exit codes when the exception occurs
  3. Monitor memory usage of both parent and child processes
  4. Review the serialVersionUID values and ensure consistency between processes
  5. Examine the JVM crash logs (hs_err_pid files) for any native crashes

Would you like me to help implement some debugging code or investigate any of these specific hypotheses further?

tnelson: The error occurs after a specific button is pressed: when (but may not be caused by) Z3 being invoked. The concrete exception is: java.io.StreamCorruptedException: invalid type code: 23 New file: `hs_err_pid33622.log ` in the OldCompoSAT directory. implications of that type code? useful information in the error log?

GitHub Copilot: The type code 23 in the StreamCorruptedException is very revealing! Let me examine the error log and analyze what this means. Let me check the end of the log for any additional information: Now let me also look at the Z3 code path that’s mentioned in the crash: Perfect! Now I have a clear picture of what’s happening. Let me provide a comprehensive analysis:

Analysis of StreamCorruptedException with Type Code 23

Critical Discovery: This is NOT a serialization issue!

The error log reveals the root cause - the subprocess is crashing with a SIGSEGV in the native Z3 library, which corrupts the object stream.

Type Code 23 Meaning:

In Java’s ObjectStreamConstants, type code 23 (0x17) corresponds to TC_REFERENCE. When you see “invalid type code: 23”, it means the ObjectInputStream expected a valid object stream header but instead read corrupted data from the crashed subprocess.

What Actually Happened:
  1. Z3 Native Library Crash: The subprocess crashed with SIGSEGV in Z3_optimize_check+0x68 in libz3.dylib
  2. Incomplete Write: The crash occurred while the subprocess was in the middle of writing serialized data to its stdout
  3. Stream Corruption: The parent process’s ObjectInputStream.readObject() received partial/corrupted data instead of a complete serialized object
  4. Type Code Error: The incomplete data stream contained byte value 23 where the stream parser expected a valid type code
The Call Stack Shows:
Z3_optimize_check (CRASHED)
↓
com.microsoft.z3.Native.optimizeCheck
↓  
com.microsoft.z3.Optimize.Check()
↓
edu.mit.csail.sdg.alloy4whole.CoverageStruct.getQueue()
↓
SimpleReporter$SimpleTask2.run() (in subprocess)
↓
WorkerEngine thread trying to read response (FAILS with StreamCorruptedException)
Key Evidence:
  • Architecture Mismatch: The log shows arm64 (Apple Silicon) but you mentioned “Intel macs” - this suggests either a platform mismatch or Rosetta translation issues
  • Native Library Issue: The crash is in the native Z3 library at libz3.dylib+0x57120
  • Memory Access Violation: SIGSEGV with SEGV_ACCERR indicates bad memory access in Z3
  • Timing: The crash occurred at exactly 6.19 seconds into execution during Z3 optimization
Root Causes (in order of likelihood):
  1. Architecture Mismatch: Z3 native library compiled for different architecture than runtime
  2. Z3 Library Bug: Native crash in Z3’s optimization routines
  3. Memory Corruption: Z3 accessing invalid memory, possibly due to concurrent access or initialization issues
  4. Library Version Incompatibility: Z3 Java bindings vs native library version mismatch
Diagnostic Questions:

  1. Platform: You mentioned “Intel macs” but the log shows arm64. Are you running this on Apple Silicon with Rosetta, or is there a platform mismatch?

  2. Z3 Installation: How was Z3 installed? Are the Java bindings (com.microsoft.z3.jar) and native library (libz3.dylib) from the same Z3 build/version?

  3. Concurrency: Is this happening during concurrent Z3 operations, or during the first Z3 call?

Immediate Fixes to Try:
  1. Check Z3 Architecture: Ensure Z3 native libraries match your runtime architecture
  2. Update Z3: Try a newer/different version of Z3
  3. Add Native Crash Handling: Wrap Z3 calls in try-catch and handle native crashes gracefully
  4. Z3 Initialization: Ensure Z3 is properly initialized before optimization calls

The StreamCorruptedException: invalid type code: 23 is just a symptom - the real problem is the Z3 native library crash that’s corrupting the inter-process communication stream.

tnelson: The z3 dylib files are universal, and we rebuilt them recently. But the com.microsoft.z3.jar was NOT rebuilt, we're using the older version. Steps to discover if there is some important mismatch between the dylibs and the jar?

GitHub Copilot: Excellent insight! A mismatch between the native Z3 libraries and the Java bindings is a very likely cause of the native crash. Let me help you investigate this version mismatch. Let me extract and examine the Z3 JAR file to get version information: The JAR is quite old (from 2018). Let me now check the Z3 dylib version and look for version information in the Java classes: Perfect! Now let me check the Z3 native library version:

tnelson: I believe the code is loading the version in bin/x86-mac -- but this is universal, so should be OK for both architectures

GitHub Copilot: You’re right! Let me check what the crash log showed about the library path and then examine the x86-mac versions that are actually being loaded: The crash log shows it’s loading from a temp directory. Let me check what’s in the x86-mac directory (which should be universal) and verify the library versions: Great! The x86-mac version is indeed universal. Now let me extract the version information from the Z3 native libraries and compare with the JAR: Excellent! The native library is Z3 4.5.1.0. Now let me check what version the Java JAR expects by looking at the Native class: Let me create a simple test to check what version the JAR is actually expecting:

Made changes.

Right, it needs the libz3java library. Let me check what libraries are actually being copied to that temp directory during the process launch: Now let me look at SimpleGUI.java to see how it sets up the Z3 libraries: Perfect! I can see that the Z3 libraries are being copied. Let me check what arch resolves to: Ah! There’s the key insight. On line 379, it forces arch="x86-mac" for all Mac systems, stating “our pre-compiled binaries are all universal binaries”. So it should be loading from bin/x86-mac/.

Now let me check if there are any API differences between the JAR version and the native library. The quickest way is to look for the specific function that crashed: Great! The Z3_optimize_check function exists at address 000000000005680c. Now let me check what functions the Java JAR is expecting: Perfect! The Java JAR expects INTERNALoptimizeCheck(JJ)I which should map to Z3_optimize_check in the native library. Now let me check the actual function signature and parameter mismatch by looking at the libz3java.dylib: Excellent! I can see both the JNI bridge function _Java_com_microsoft_z3_Native_INTERNALoptimizeCheck at address aa28 and the undefined external symbol _Z3_optimize_check that it should call.

Let me now use a better approach to compare the actual Z3 versions. I’ll create a simple program that just tries to call the Z3 version functions: Let me check what classes are available: Now let me create a test that specifically tests the broken function path:

The issue is that it can’t find libz3java. This suggests there might be a naming issue. Let me check the actual library loading in the Native class: Notice that the libz3java.dylib expects to find libz3.dylib in the same directory (no absolute path). This is a critical version compatibility indicator!

Findings and Diagnosis Steps

Based on my investigation, here are the key steps to discover the version mismatch:

1. Version Dating Evidence:
  • JAR file: Created January 11, 2018 (based on unzip -l output)
  • Native Libraries: August 3, 2025 (recently rebuilt universal binaries)
  • 7+ year gap between JAR and native libraries
2. Z3 Version Analysis:
  • Native Z3 Version: 4.5.1.0 (from strings output)
  • JAR Build Date: 4.3.2 (from MANIFEST.MF: “Created-By: 4.3.2 (Microsoft Research LTD.)”)
3. Function Signature Compatibility:

The native library does have all the expected optimize functions, but the version mismatch may cause:

  • ABI changes in function signatures
  • Memory layout differences in Z3 internal structures
  • Calling convention changes between Z3 4.3.2 and 4.5.1.0
4. Definitive Version Mismatch Test:

To confirm the exact version incompatibility, create this diagnostic:

Made changes.

🚨 CRITICAL VERSION MISMATCH DISCOVERED! 🚨

Confirmed Evidence:
  1. JAR Version: Z3 4.3.2 (January 2018)
  2. Native Library: Z3 4.12.2.0 (August 2025) - Not 4.5.1.0 as I initially saw
  3. Function Mismatch: JAR expects 48 optimize functions, native library provides 28
Root Cause:

The 7+ year version gap between Z3 4.3.2 (JAR) and Z3 4.12.2.0 (native libraries) has introduced significant API changes:

  • Missing/renamed functions
  • Changed function signatures
  • Modified internal data structures
  • Different calling conventions
The Fix:

You need to rebuild the com.microsoft.z3.jar to match your Z3 4.12.2.0 native libraries, or downgrade your native libraries to match the Z3 4.3.2 JAR.

Recommended approach: Download/rebuild the Z3 4.12.2.0 Java bindings to match your recently built native libraries.

The StreamCorruptedException: invalid type code: 23 was indeed caused by the subprocess crashing due to this fundamental version incompatibility in the Z3 optimize functions!

tnelson: will the versions be the same between the x86 and arm64 parts of each universal dylib? They were combined via lipo, so we should check

GitHub Copilot: Great point! When libraries are combined with lipo, each architecture slice can have different versions. Let me check if the x86_64 and arm64 parts of the universal dylibs have the same Z3 versions: 🎯 BINGO! This is the smoking gun!

Critical Discovery: Architecture-Specific Version Mismatch

The universal binary has different Z3 versions per architecture:

  • x86_64 slice: Z3 4.5.1.0
  • arm64 slice: Z3 4.12.2.0

Since you’re running on Apple Silicon (as shown in the crash log: arm64), the system is using the arm64 slice with Z3 4.12.2.0, but your Java JAR is from Z3 4.3.2 (2018).

Let me also check the libz3java.dylib: Now let me test which architecture slice your system would actually use by running a quick test: Perfect! Let me create an updated comprehensive diagnostic:

Made changes.

🎯 Complete Diagnosis Summary

Root Cause Confirmed:

Your lipo-combined universal binary has different Z3 versions per architecture:

  • JAR: Z3 4.3.2 (January 2018)
  • x86_64 slice: Z3 4.5.1.0 (closer but still mismatched)
  • arm64 slice: Z3 4.12.2.0 ⬅️ This is what’s being used and crashing
Why the Crash Happens:
  1. Your Apple Silicon Mac runs the arm64 slice (Z3 4.12.2.0)
  2. The Java JAR expects Z3 4.3.2 APIs
  3. 4+ years of API evolution between versions creates incompatible function signatures
  4. When INTERNALoptimizeCheck calls Z3_optimize_check, the parameters/structures don’t match
  5. This causes the SIGSEGV in Z3_optimize_check+0x68
  6. The subprocess crash corrupts the ObjectInputStream
  7. Parent gets StreamCorruptedException: invalid type code: 23
Quick Fix Options:

Option 1 (Fastest): Force x86_64 usage via Rosetta:

arch -x86_64 java -cp .:lib/com.microsoft.z3.jar -Djava.library.path=bin/x86-mac YourProgram

Option 2 (Proper): Rebuild the Z3 Java bindings for version 4.12.2.0

Option 3: Replace the arm64 slice with a compatible version

The version mismatch between your universal binary’s architecture slices is the definitive cause of your Z3 crashes and subsequent stream corruption!