diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc index e36b6e31650..bdfb938fb45 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc +++ b/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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc b/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc index 7d75cd82796..414f2523540 100644 --- a/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc +++ b/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.