Make get_array return nil for long strings

Instead of aborting the program when the string is too long, we consider
this happened because of some invalid object, and return nil as a model
of the array.
Access to this invalid object is prevented by other part of the code and
should not occur in the trace.

Author: romainbrenguier

regression/jbmc-strings/long_string/test_abort.desc

@@ -1,9 +1,10 @@
 CORE
 Test.class
---refine-strings --function Test.checkAbort
-^EXIT=6$
+--refine-strings --function Test.checkAbort --trace
+^EXIT=10$
 ^SIGNAL=0$
+dynamic_object[0-9]*=\(assignment removed\)
 --
 --
-This tests should abort, because concretizing a string of the required
-length may take to much memory.
+This tests that the object does not appear in the trace, because concretizing
+a string of the required length may take too much memory.

src/solvers/refinement/string_refinement.cpp

@@ -933,12 +933,17 @@ static optionalt<exprt> get_array(
 
   if(n > MAX_CONCRETE_STRING_SIZE)
   {
-    stream << "(sr::get_array) long string (size=" << n << ")" << eom;
-    std::ostringstream msg;
-    msg << "consider reducing string-max-input-length so that no string "
-        << "exceeds " << MAX_CONCRETE_STRING_SIZE << " in length and make sure"
-        << " all functions returning strings are available in the classpath";
-    throw string_refinement_invariantt(msg.str());
+    stream << "(sr::get_array) long string (size " << format(arr.length())
+           << " = " << n << ") " << format(arr) << eom;
+    stream << "(sr::get_array) consider reducing string-max-input-length so "
+              "that no string exceeds "
+           << MAX_CONCRETE_STRING_SIZE
+           << " in length and "
+              "make sure all functions returning strings are loaded"
+           << eom;
+    stream << "(sr::get_array) this can also happen on invalid object access"
+           << eom;
+    return nil_exprt();
   }
 
   if(