Currently, some of the fresh variables are not prefixed with the function names which would break jdiff if string processing was required to be used there, e.g. https://github.com/diffblue/cbmc/blob/develop/jbmc/src/java_bytecode/java_string_library_preprocess.cpp#L266