Merge pull request #6849 from tautschnig/cleanup/solver-indep-tests

Tests: do not unnecessarily constrain what models solvers can produce [blocks: #6439]

Author: tautschnig

jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc

@@ -1,6 +1,6 @@
 CORE
 Main
---function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+--function Main.nondetArg --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc

@@ -1,6 +1,6 @@
 CORE
 Main
---function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+--function Main.noprop --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc-library/free-01/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check --stop-on-fail
-free argument must be NULL or valid pointer
+free argument must be (NULL or valid pointer|dynamic object)
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$