`jbmc --trace` prints millions of unknown characters for nondeterministic strings

[lemmy]

JBMC 6.11 expands a nondeterministic string’s entire backing character array when printing a counterexample trace.

Reproducer:

public final class JbmcTraceReproducer {
    public static void verify() {
        final String name = JbmcTraceReproducer.class.getName();
        assert name.length() < 4_194_304;
    }
}

javac JbmcTraceReproducer.java

# Prints 4,194,304 "'?'," entries.
jbmc 'JbmcTraceReproducer.verify:()V' --classpath . --property 'java::JbmcTraceReproducer.verify:()V.assertion.1' --trace

This was found while using JBMC to verify TLC’s IntervalValue in tlaplus/tlaplus#1441. JBMC found the expected overflow counterexample, but rendering its trace exposed this issue. Environment: JBMC/CBMC 6.11.0, macOS arm64.