Limit counterexample size to speed up regression tests

These regression tests only require 1-2 seconds of solving time, but may
produce counterexample traces that are greater than 8 GB on disk. Limit
the maximum string length (in none of the tests does the length even
matter) to avoid such artificial blow-up. Also, these tests were
possibly a lot slower with other solvers, simply because these would
produce different models. Before this PR, we had:
* assume-inputs-non-null/string_assume.desc:
** cadical: 165 seconds
** minisat: 0 seconds
* context-include-exclude/test_exclude_from_include.desc:
** cadical: 796 seconds
** minisat: 1 seconds
* context-include-exclude/test_include.desc:
** cadical: 802 seconds
** minisat: 1 seconds
* exceptions29/test.desc:
** cadical: 168 seconds
** minisat: 0 seconds
when the actual solver time was less than 2 seconds.

Author: tautschnig

jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 My
---function My.stringArg --java-assume-inputs-non-null
+--function My.stringArg --java-assume-inputs-non-null --max-nondet-string-length 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
@@ -10,6 +10,3 @@ My
 ^warning: ignoring
 --
 Check that --java-assume-inputs-non-null restricts inputs to non-null strings
-
-The test is marked "THOROUGH" as it requires more memory than may be available
-on some GitHub runners.

jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Main
---context-include Main.main --context-include 'Main.<clinit' --context-include org.cprover.MyClass --context-exclude 'org.cprover.MyClass$Inner.'
+--context-include Main.main --context-include 'Main.<clinit' --context-include org.cprover.MyClass --context-exclude 'org.cprover.MyClass$Inner.' --max-nondet-string-length 10
 ^EXIT=10$
 ^SIGNAL=0$
 .* line 12 assertion at file Main.java line 12 .*: FAILURE
@@ -12,6 +12,3 @@ WARNING: no body for function .*
 --
 Tests that only the specified methods and classes are included, while
 the inner class from MyClass is excluded.
-
-The test is marked "THOROUGH" as it requires more memory than may be available
-on some GitHub runners.

jbmc/regression/jbmc/context-include-exclude/test_include.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Main
---context-include Main.
+--context-include Main. --max-nondet-string-length 10
 ^EXIT=10$
 ^SIGNAL=0$
 .* line 12 assertion at file Main.java line 12 .*: SUCCESS
@@ -11,6 +11,3 @@ Main
 WARNING: no body for function .*
 --
 Tests that only methods from the specified class are included.
-
-The test is marked "THOROUGH" as it requires more memory than may be available
-on some GitHub runners.

jbmc/regression/jbmc/exceptions29/test.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 test
---unwind 10
+--unwind 10 --max-nondet-string-length 10
 ^\[java::test.main:\(\[Ljava/lang/String;\)V\.assertion.1\] line 14 assertion at file test\.java line 14 function java::test.main:\(\[Ljava/lang/String;\)V bytecode-index 21: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
@@ -15,6 +15,3 @@ test.main gives the following exception table:
     8    22    25   Class java/lang/Exception
     0     7    45   Class MyException
     8    42    45   Class MyException
-
-The test is marked "THOROUGH" as it requires more memory than may be available
-on some GitHub runners.