Skip to content

Commit 0040a7d

Browse files
committed
Fix String test off-by-one error
This was incidentally exposed by the previous commit; due to comparing with < against a limit enforced with > in the string solver, it always had the possibility not to abort as the test expects.
1 parent e3d29a0 commit 0040a7d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

regression/jbmc-strings/long_string/Test.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ public static void checkAbort(String s, String t) {
3030
String u = s.concat(t);
3131

3232
// Filter out
33-
if(u.length() < 67_108_864)
33+
if(u.length() <= 67_108_864)
3434
return;
3535
if(CProverString.charAt(u, 2_000_000) != 'b')
3636
return;

0 commit comments

Comments
 (0)