Skip to content

Commit 48e5b25

Browse files
smowtonsmowton
committed
Amend faulty long-string test
This test previously checked that the *sum* of the arguments' sizes didn't exceed some critical bound, but this didn't exclude the case where one of them is just within bounds (but still long enough to cause a memout when we try to concretise it) and the other just long enough to push the sum over the boundary. Instead we'll check that one or the other is very long, and the other one acceptably short.
1 parent 3f718ba commit 48e5b25

File tree

2 files changed

+6
-1
lines changed

2 files changed

+6
-1
lines changed

‎regression/jbmc-strings/long_string/Test.class‎

200 Bytes
Binary file not shown.

‎regression/jbmc-strings/long_string/Test.java‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,12 @@ public static void checkAbort(String s, String t) {
3232
// Filter out
3333
// 67_108_864 corresponds to the maximum length for which the solver
3434
// will concretize the string.
35-
if(u.length() <= 67_108_864)
35+
if(s.length() <= 67_108_864 && t.length() <= 67_108_864)
36+
return;
37+
// Check at least one of them is short-ish, so we don't end up trying
38+
// to concretise a very long but *just* allowable string and memout the
39+
// test infrastructure:
40+
if(s.length() > 1024 && t.length() > 1024)
3641
return;
3742
if(CProverString.charAt(u, 2_000_000) != 'b')
3843
return;

0 commit comments

Comments
 (0)