From 367340b3204d939753cf3c04a56cda94da57cfef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 May 2023 10:25:35 +0000 Subject: [PATCH] Limit string length to avoid spurious regression test failure As seen in https://github.com/diffblue/cbmc/actions/runs/4979949266/jobs/8933402303?pr=7413 we may end up with a counterexample too large store on GitHub's runner. Limit the string length as the length is immaterial to the test. --- jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc index 4e07e36aac7..7ad022e0f81 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-non-null +--function My.classArg --java-assume-inputs-non-null --max-nondet-string-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$