Unexpected results when the targeted class has an inner class

[zzctmac]

The first class with expected results is as follows:

public class Testee {
    private static final List<Locale> AVAILABLE_LOCALE_LIST;

    static {
        // extra safe
        final List<Locale> list = new ArrayList<Locale>(Arrays.asList(Locale.getAvailableLocales()));
        AVAILABLE_LOCALE_LIST = Collections.unmodifiableList(list);
    }

    public static List<Locale> availableLocaleList() {
        return AVAILABLE_LOCALE_LIST;
    }

    static public void assertNullOrEmpty() { // whether the return is null or empty.
        List<Locale> ret = availableLocaleList();
        ass3rt(ret == null || ret.isEmpty());
    }
}

When I run the following main method:

public static void main(String[] args) {
        final RunParameters p = new RunParameters();
        p.addUserClasspath("./target/classes");
        p.setJBSELibPath(System.getenv("JBSE_LIB"));
        p.setMethodSignature("Testee", "()V", "assertNullOrEmpty");
        p.setDecisionProcedureType(Z3);
        p.getRunnerParameters().getEngineParameters().setMakePreInitClassesSymbolic(false);
        p.setExternalDecisionProcedurePath(System.getenv("JBSE_Z3_PATH"));
        p.setOutputFilePath("./out/TesteeAssertNullOrEmpty.txt");
        p.setStateFormatMode(PATH);
        p.setStepShowMode(LEAVES);
        final jbse.apps.run.Run r = new jbse.apps.run.Run(p);
        r.run();
    }

JBSE gives me the correct results:

This is the Java Bytecode Symbolic Executor's Run Tool (Assembles a jar archive containing the classes of the 'main' feature. v.0.11.0-SNAPSHOT).
Connecting to Z3 at /path/z3.
Starting symbolic execution of method Testee:()V:assertNullOrEmpty at Wed Mar 27 15:13:53 CST 2024.
.1[22] 0,24 LEAF 
.1[22] path violates an assertion.
Symbolic execution finished at Wed Mar 27 15:14:03 CST 2024.
Analyzed states: 5497781, Analyzed pre-initial states: 5497759, Analyzed paths: 1, Safe: 0, Unsafe: 1, Out of scope: 0, Violating assumptions: 0, Unmanageable: 0.
Elapsed time: 10 sec 267 msec, Elapsed pre-initial phase time: 10 sec 262 msec, Average speed: 535480 states/sec, Average post-initial phase speed: 4400 states/sec, Elapsed time in decision procedure: 173 msec (1.69% of total).

The JBSE results show that there is an Unsafe path, which means that the return of availableLocaleList method can be non-empty.

However, After modifying the class into the following one with an inner class:

public class TesteeWithInnerClass {
    static class SyncAvoid {

        /**
         * Unmodifiable list of available locales.
         */
        private static final List<Locale> AVAILABLE_LOCALE_LIST;

        /**
         * Unmodifiable set of available locales.
         */

        static {
            // extra safe
            final List<Locale> list = new ArrayList<Locale>(Arrays.asList(Locale.getAvailableLocales()));
            AVAILABLE_LOCALE_LIST = Collections.unmodifiableList(list);
        }
    }
    public static List<Locale> availableLocaleList() {
        return SyncAvoid.AVAILABLE_LOCALE_LIST;
    }

    static public void assertNullOrEmpty() {
        List<Locale> ret = availableLocaleList();
        ass3rt(ret == null || ret.isEmpty());
    }
}

When I run the following main method:

 public static void main(String[] args) {
        final RunParameters p = new RunParameters();
        p.addUserClasspath("./target/classes");
        p.setJBSELibPath(System.getenv("JBSE_LIB"));
        p.setMethodSignature("TesteeWithInnerClass", "()V", "assertNullOrEmpty");
        p.setDecisionProcedureType(Z3);
        //p.setMakePreInitClassesSymbolic(true);
        p.getRunnerParameters().getEngineParameters().setMakePreInitClassesSymbolic(false);
        p.setExternalDecisionProcedurePath(System.getenv("JBSE_Z3_PATH"));
        p.setOutputFilePath("./out/TesteeWithInnerClassAssertNullOrEmpty.txt");
        p.setStateFormatMode(PATH);
        p.setStepShowMode(LEAVES);
        final jbse.apps.run.Run r = new jbse.apps.run.Run(p);
        r.run();
    }

JBSE gives me the incorrect results:

This is the Java Bytecode Symbolic Executor's Run Tool (Assembles a jar archive containing the classes of the 'main' feature. v.0.11.0-SNAPSHOT).
Connecting to Z3 at /path/z3.
Starting symbolic execution of method TesteeWithInnerClass:()V:assertNullOrEmpty at Wed Mar 27 15:24:17 CST 2024.
.1[3] [TesteeWithInnerClass$SyncAvoid].TesteeWithInnerClass$SyncAvoid:AVAILABLE_LOCALE_LIST not expanded, because no concrete, compatible, pre-initialized class was found.
.1[15] 1,13 LEAF 
.1[15] path is safe.
Symbolic execution finished at Wed Mar 27 15:24:20 CST 2024.
Analyzed states: 717531, Analyzed pre-initial states: 717516, Analyzed paths: 1, Safe: 1, Unsafe: 0, Out of scope: 0, Violating assumptions: 0, Unmanageable: 0.
Elapsed time: 2 sec 419 msec, Elapsed pre-initial phase time: 2 sec 403 msec, Average speed: 296622 states/sec, Average post-initial phase speed: 937 states/sec, Elapsed time in decision procedure: 23 msec (0.95% of total).

It cannot find the Unsafe path.

Meanwhile, when I uncomment p.setMakePreInitClassesSymbolic(true);, the results are not changed.

[zzctmac]

My JAVA version is 1.8.0_281, and the machine is a MacBook with an Intel CPU.