CORE
Test.class
--function Test.check
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
file Test.java line 20 .*: FAILURE$
--
--
--max-nondet-string-length is not used on purpose, because this tests the behaviour
of string refinement on very large strings.
