From aa766ae3af7e1949860a6d35c2fcb6fbe7303b31 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 27 Mar 2018 15:58:57 +0100 Subject: [PATCH] Set string-max-length in indexOf test Without this, the solver can end up with a difficult instance for minisat. This behavior depends on the envioronment in which CBMC/JBMC is build, for instance travis and appVeyor may get different counter-examples from the SAT-solver, because of slightly different inputs. The behavior can also vary from one commit to the other on the same system (even if the changes seem unrelated to the solvers). However running the same benchmark on the same operating system with the same version of CBMC/JBMC should always behave the same. --- regression/jbmc-strings/StringIndexOf/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc index 2e22278a15b..74cda5ee46b 100644 --- a/regression/jbmc-strings/StringIndexOf/test.desc +++ b/regression/jbmc-strings/StringIndexOf/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null +--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --string-max-length 100 --java-assume-inputs-non-null ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$