Amend faulty long-string test

This test previously checked that the *sum* of the arguments' sizes didn't
exceed some critical bound, but this didn't exclude the case where one of them
is just within bounds (but still long enough to cause a memout when we try to
concretise it) and the other just long enough to push the sum over the boundary.

Instead we'll check that one or the other is very long, and the other one acceptably
short.

Author: smowton

regression/jbmc-strings/long_string/Test.class

@@ -32,7 +32,12 @@ public static void checkAbort(String s, String t) {
         // Filter out
         // 67_108_864 corresponds to the maximum length for which the solver
         // will concretize the string.
-        if(u.length() <= 67_108_864)
+        if(s.length() <= 67_108_864 && t.length() <= 67_108_864)
+            return;
+        // Check at least one of them is short-ish, so we don't end up trying
+        // to concretise a very long but *just* allowable string and memout the
+        // test infrastructure:
+        if(s.length() > 1024 && t.length() > 1024)
             return;
         if(CProverString.charAt(u, 2_000_000) != 'b')
             return;