Add models to jbmc String.hashCode test

The model will become necessary as we remove the preprocessing for
hashCode and replace it with a model.

Author: romainbrenguier

jbmc/regression/strings-smoke-tests/java_hash_code/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_hash_code.class
---max-nondet-string-length 1000 --function test_hash_code.main
+--max-nondet-string-length 1000 --function test_hash_code.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$