Skip to content

Commit f9caf41

Browse files
Strengthen condition in TokenTest02 and reduce unwind
The check for VERIFICATION FAILED could match a null pointer check rather than an assertion.
1 parent 3635419 commit f9caf41

File tree

1 file changed

+2
-1
lines changed
  • jbmc/regression/jbmc-strings/TokenTest02

1 file changed

+2
-1
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
CORE
22
TokenTest02.class
3-
--max-nondet-string-length 1000 --unwind 15 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--max-nondet-string-length 1000 --unwind 6 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7+
line 13 assertion at file TokenTest02\.java .*: FAILURE
78
--
89
^warning: ignoring

0 commit comments

Comments
 (0)