Package_friendly loads the java_languaget twice which creates problems when there are models.

[dcattaruzza]

Dual loading of java_bytecode_language causes duplicate attempt to create the clinit of model classes, which violates an invaraint. The loading should be done on a single instance.

See regression/cbmc-java/package_friendly1/test.desc for a failing test.