Merge pull request #4896 from yumibagge/yb/jbmc-regression-multi-dimentional-char-array

Add KNOWNBUG for multidimentional char array[TG-8466]

Author: tautschnig

jbmc/regression/jbmc/multidimensional-array-char/My.class

@@ -0,0 +1,19 @@
+public class My {
+  public int check2DCharArray(char[][] board, boolean assertionCheck) {
+    int diff = 0;
+    for (int row = 0; row < 2; row++) {
+      for (int col = 0; col < 2; col++) {
+        if (board[row][col] == 'O') {
+          diff++;
+          assert !assertionCheck;
+          assert diff < 10;
+        } else if (board[row][col] == 'X') {
+          diff--;
+          assert !assertionCheck;
+          assert diff < 10 ;
+        }
+      }
+    }
+    return diff;
+  }
+}

jbmc/regression/jbmc/multidimensional-array-char/My.java

@@ -0,0 +1,15 @@
+KNOWNBUG
+My.class
+--function My.check2DCharArray --unwind 5 --max-nondet-array-length 10
+line 8 assertion at file My.java.*: FAILURE
+line 9 assertion at file My.java.*: SUCCESS
+line 12 assertion at file My.java.*: FAILURE
+line 13 assertion at file My.java.*: SUCCESS
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Multidimentional char array used to cause a performance issue which is reported
+in TG-5076. The issue is no longer reproducible.
+It currently core-dump jbmc by generating invalid trace: TG-8466