Skip to content

Commit a0e339d

Browse files
committed
Disable broken string test
This currently breaks an assertion as described in the .desc file. It should be re-enabled once string-refinement knows how to introduce sufficient indirection to overcome this.
1 parent d0cf433 commit a0e339d

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1-
CORE
1+
KNOWNBUG
22
Test.class
33
--max-nondet-string-length 100 --unwind 10 --function Test.checkNonDet
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion at file Test.java line 66 .*: SUCCESS
77
assertion at file Test.java line 69 .*: FAILURE
88
--
9+
--
10+
The nondet test currently breaks the invariant at string_refinement.cpp:2162
11+
("Indices not equal..."), which checks that a given string is not used with
12+
multiple distinct indices. As the test checks s.substring(s, 1), two distinct
13+
indices are indeed used.

0 commit comments

Comments
 (0)