Fix NoSuchFieldError in Java JNI wrapper for BOOL OUT/INOUT parameters

[Copilot]

The JNI code generator incorrectly treated BOOL OUT/INOUT parameters identically to INT/UINT, using field descriptor "I" and SetIntField — but BoolPtr.value is declared boolean (JNI type "Z"), causing java.lang.NoSuchFieldError at runtime.

Changes

• scripts/update_api.py: Split BOOL out from the INT/UINT branch in the OUT/INOUT parameter write-back section. BOOL parameters now emit "Z" as the JNI field descriptor and call SetBooleanField, matching the BoolPtr Java class definition.

// Before (broken): treated bool* the same as int*
jfieldID fid = jenv->GetFieldID(mc, "value", "I");
jenv->SetIntField(a2, fid, (jint) _a2);

// After (fixed): correct field type for boolean
jfieldID fid = jenv->GetFieldID(mc, "value", "Z");
jenv->SetBooleanField(a2, fid, (jboolean) _a2);

This affects Z3_fpa_get_numeral_sign and all other API functions with bool* OUT/INOUT parameters (e.g. the four BoolPtr params in Z3_rcf_interval).

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Regression: NoSuchFieldError in Java API for fpaGetNumeralSign due to BoolPtr mismatch</issue_title>
<issue_description>### Description
A regression was introduced in 4af83e8 where the Java API now uses BoolPtr in fpaGetNumeralSign. The generated JNI code incorrectly attempts to access an integer field ("I") on a boolean pointer object, resulting in a java.lang.NoSuchFieldError.

Reproduction Example

The following Java snippet triggers the crash:

    long cfg = Native.mkConfig();
    final long context = Native.mkContextRc(cfg);
    long fpSort = Native.mkFpaSort(context, 5, 10);
    long fpNum = Native.mkFpaNumeralInt(context, 12, fpSort);
    Native.incRef(context, Native.sortToAst(context, fpNum));
    Native.BoolPtr signPtr = new Native.BoolPtr();
    Native.fpaGetNumeralSign(context, fpNum, signPtr); // <-- crash

Stack Trace:

java.lang.NoSuchFieldError: com.microsoft.z3.Native$BoolPtr.value I
	at com.microsoft.z3.Native.INTERNALfpaGetNumeralSign(Native Method)
	at com.microsoft.z3.Native.fpaGetNumeralSign(Native.java:7540)

Description and Source of the Regression / Bug

With the changes of 4af83e8, the generated JNI code for INTERNALfpaGetNumeralSign treats BoolPtr as if it contains an integer value field:

DLL_VIS JNIEXPORT jboolean JNICALL Java_com_microsoft_z3_Native_INTERNALfpaGetNumeralSign(JNIEnv * jenv, jclass cls, jlong a0, jlong a1, jobject a2) {
  bool _a2;
  bool result = Z3_fpa_get_numeral_sign((Z3_context)a0, (Z3_ast)a1, &_a2);
  {
     jclass mc    = jenv->GetObjectClass(a2);
     jfieldID fid = jenv->GetFieldID(mc, "value", "I");    // <-- access to int field crashes with NoSuchFieldError, required value "Z" for Boolean
     jenv->SetIntField(a2, fid, (jint) _a2);               // <-- another bug: cast to jint instead of jboolean?
  }
  return (jboolean) result;
}

The api-generator script for that exact binding is located in

z3/scripts/update_api.py

Lines 855 to 860 in 96285b0

	if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
	java_wrapper.write(' {\n')
	java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
	java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
	java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
	java_wrapper.write(' }\n')

.
We propose a change as follows:

-                if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
+                if param_type(param) == INT or param_type(param) == UINT:
                     java_wrapper.write('  {\n')
                     java_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
                     java_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
                     java_wrapper.write('     jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
                     java_wrapper.write('  }\n')
+                elif param_type(param) == BOOL:
+                    java_wrapper.write('  {\n')
+                    java_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
+                    java_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "Z");\n')
+                    java_wrapper.write('     jenv->SetIntField(a%s, fid, (jboolean) _a%s);\n' % (i, i))
+                    java_wrapper.write('  }\n')
                 elif param_type(param) == STRING:

Additional Consideration due to Unclear Dependency

The method Z3_rcf_interval has four parameters of type BoolPtr. Please check if that previously worked in Java via JNI or not. The proposed change might either fix or break it. This should be tested!

References

This regression was found while updating Z3 in JavaSMT: sosy-lab/java-smt#609 from older v4.15.4 which is the working base version here.
This issue appears with several releases of Z3:

• v4.15.5,
• v4.15.6,
• v4.15.7,
• v4.15.8, and
• v4.16.0.</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Regression: NoSuchFieldError in Java API for fpaGetNumeralSign due to BoolPtr mismatch #8831

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.