diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc index b4db9cfcef3..a7f4773db73 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc +++ b/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$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc index bdddbfaed8f..068164f2d7b 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc +++ b/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$ diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc index 769ba573e7c..a727d0817d0 100644 --- a/regression/cbmc-library/free-01/test.desc +++ b/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$