Skip to content

Commit a630bb7

Browse files
Correct bound in test with long string
To make the solver abort the length has to be strictly greater than 2^26.
1 parent 1776a9e commit a630bb7

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed
0 Bytes
Binary file not shown.

regression/jbmc-strings/long_string/Test.java

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,9 @@ 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+
// 67_108_864 corresponds to the maximum length for which the solver
34+
// will concretize the string.
35+
if(u.length() <= 67_108_864)
3436
return;
3537
if(CProverString.charAt(u, 2_000_000) != 'b')
3638
return;

0 commit comments

Comments
 (0)