smowton
diff --git a/‎.travis.yml
+17-5 b/‎.travis.yml
+17-5
diff --git a/‎COMPILING.md
+13-4 b/‎COMPILING.md
+13-4
diff --git a/‎appveyor.yml
+8-12 b/‎appveyor.yml
+8-12
diff --git a/‎regression/cbmc-cover/built-ins7/test.desc
+4-1 b/‎regression/cbmc-cover/built-ins7/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc1/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc1/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc10/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc10/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc11/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc11/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc12/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc12/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc13/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc13/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc14/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc14/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc2/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc2/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc3/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc3/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc4/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc4/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc5/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc5/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc6/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc6/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc7/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc7/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc8/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc8/test.desc
+4-1
diff --git a/‎regression/cbmc-cover/mcdc9/test.desc
+4-1 b/‎regression/cbmc-cover/mcdc9/test.desc
+4-1
diff --git a/‎regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class
619 Bytes b/‎regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class
619 Bytes
diff --git a/‎regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java
+11 b/‎regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java
+11
diff --git a/‎regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class
232 Bytes b/‎regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class
232 Bytes
diff --git a/‎regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java
+4 b/‎regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java
+4
diff --git a/‎regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class
219 Bytes b/‎regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class
219 Bytes
diff --git a/‎regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java
+4 b/‎regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java
+4
diff --git a/‎regression/cbmc-java/ArithmeticException7/test.desc
+9 b/‎regression/cbmc-java/ArithmeticException7/test.desc
+9
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class
642 Bytes b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class
642 Bytes
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java
+11 b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java
+11
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class
263 Bytes b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class
263 Bytes
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java
+4 b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java
+4
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class
244 Bytes b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class
244 Bytes
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java
+4 b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java
+4
diff --git a/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class
219 Bytes b/‎regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class
219 Bytes
@@ -65,7 +65,9 @@ jobs:
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER="ccache g++-5"
+      env:
+        - COMPILER="ccache g++-5"
+        - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
 
     # OS X using g++
     - stage: Test different OS/CXX/Flags
@@ -115,7 +117,7 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
-    # Ubuntu Linux with glibc using clang++-3.7
+    # Ubuntu Linux with glibc using clang++-3.7, no-debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -138,6 +140,7 @@ jobs:
       env:
         - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
+        - EXTRA_CXXFLAGS="-DNDEBUG"
 
     # Ubuntu Linux with glibc using clang++-3.7, debug mode
     - stage: Test different OS/CXX/Flags
@@ -165,6 +168,7 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    # cmake build using g++-5
     - stage: Test different OS/CXX/Flags
       os: linux
       cache: ccache
@@ -177,20 +181,27 @@ jobs:
           packages:
             - g++-5
       install:
+        - ccache -z
+        - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
         - cmake --build build -- -j4
-      script: (cd build; ctest -V -L CORE)
+      script: (cd build; ctest -V -L CORE -j2)
 
     - stage: Test different OS/CXX/Flags
       os: osx
       cache: ccache
+      before_install:
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
+        - export PATH=/usr/local/opt/ccache/libexec:$PATH
       env:
         - BUILD_SYSTEM=cmake
         - CCACHE_CPP2=yes
       install:
+        - ccache -z
+        - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
         - cmake --build build -- -j4
-      script: (cd build; ctest -V -L CORE)
+      script: (cd build; ctest -V -L CORE -j2)
 
 
     # Run Coverity
@@ -235,6 +246,7 @@ jobs:
     - <<: *linter-stage
 
 install:
+  - ccache -z
   - ccache --max-size=1G
   - make -C src minisat2-download
   - make -C src boost-download
@@ -244,7 +256,7 @@ install:
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}"
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
   - make -C unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
 
 
@@ -137,7 +137,8 @@ We recommend Visual Studio.
 Follow these instructions:
 
 1. First install Cygwin, then from the Cygwin setup facility install the
-   following packages: `flex, bison, tar, gzip, git, make, wget, patch`.
+   following packages: `flex, bison, tar, gzip, git, make, wget, patch,
+   libwww-perl`.
 2. Get the CBMC source via
    ```
    git clone https://github.com/diffblue/cbmc cbmc-git
@@ -176,6 +177,8 @@ using "make generated_files" before opening the project.
 There is an experimental build based on CMake instead of hand-written
 makefiles. It should work on a wider variety of systems than the standard
 makefile build, and can integrate better with IDEs and static-analysis tools.
+On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't
+require manual modification of build files.
 
 1. Ensure you have all the build dependencies installed. Build dependencies are
    the same as for the makefile build, but with the addition of CMake version
@@ -195,9 +198,15 @@ makefile build, and can integrate better with IDEs and static-analysis tools.
      ```
      You shoud also install [Homebrew](https://brew.sh), after which you can
      run `brew install cmake` to install CMake.
-   - On Windows, install Cygwin, then from the Cygwin setup facility install
-     `cmake`, `flex`, `bison`, `tar`, `gzip`, `git`, `make`, `wget`, and
-     `patch`.
+   - On Windows, ensure you have Visual Studio 2013 or later installed.
+     Then, download CMake from the [official download
+     page](https://cmake.org/download).
+     You'll also need `git` and `patch`, which are both provided by the
+     [git for Windows](git-scm.com/download/win) package.
+     Finally, Windows builds of flex and bison should be installed from
+     [the sourceforge page](sourceforge.net/projects/winflexbison).
+     The easiest way to 'install' these executables is to unzip them and to
+     drop the entire unzipped package into the CBMC source directory.
    - Use of CMake has not been tested on Solaris or FreeBSD. However, it should
      be possible to install CMake from the system package manager or the
      [official download page](https://cmake.org/download) on those systems.
 
@@ -12,18 +12,14 @@ install:
     md deps
     }
     cd deps
-    if (!(Test-Path bin\bison.exe)) {
-    & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/bison-2.4.1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=JAPFzNPMJDI4IViAVlJAEc6l8aHB3k17NpZRdoWDMLbALaJNX88vfwocuezU1tfhyrSJxfo2fTK4rgP5OULkikJs7MBZI9ovp2V%2BMT6yg87KDdH9EIOlMgltGfbP%2BoZkwBY7kXb3W5puSlt4OTE%2Bw7CRlHF9MNqFXVBqVBfa%2BGw0gXDe5Jd9qV%2BvUXZzRuBl9ERSQkSD%2B%2B%2BxFo24FZoOeYkgBHJz03%2BHuIMnlmcLgneTB2aiZZU3%2B6UTPceUxLus9%2Bksb5UbqEVaVE06TIXl76VKwqAgXM2LWaNyeJDog%2BT%2BhjW4v4ypxh6mIBo5KRNXVLPc1MxSPFQB3ITlIXv9Zg%3D%3D"
-    & 7z x bison-2.4.1-bin.zip
-    }
-    if (!(Test-Path bin\flex.exe)) {
-    & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/flex-2.5.4a-1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=WriP8S047Mmq271ZHWL0MCPGx1gEFsuc%2BKMmChoXhXFRkn0GlIgCxZEiOu52ke9fT1kAvycWXePNBFAyCHjpF%2BJkXCwisQ6FLIf3NL%2F92849YgQKdJkDUOcZ%2Bh82XVTwNBrljKIkExkak7QEyhOf3buTC1oeuatCUV5Ez42RZjgtRiJaqcFW6xLbhfuVONr39KxH5hGx%2FDUi2RRXPbgoKDwavc9s56NP1rNbWMTE6NdNHzJeaf43E%2BSMemlVO%2BhhIY6W0f%2FtaQ7fYF%2F6YaqxdQ0sB8W5DnG4Hb%2F0CyQlrTZpGDXGr301rV0M4WBkYLmfauq4IyJsBaR095tXGW%2BzmA%3D%3D"
-    & 7z x flex-2.5.4a-1-bin.zip
-    }
-    if (!(Test-Path include\FlexLexer.h)) {
-    & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/flex-2.5.4a-1-lib.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=H%2FLeKGv2QqKAGDTP%2F6TYPhDzuL6K%2F5dFOt61HfYBm1vUWVUNmAYVGvUAcvnUqBnhEHwZgtc8vZt1H7k3W8azxCUc7l6ZhlCDbqQ6Mg2VhfpBaQMbL1V%2BjSq5ePpWcuLMBntKk2br38PF1NtiAwCCpRTRPptaYPeGs%2BOjAH%2BN8aIIxjvj45QAgt9mcg6dfBsyfj5fdJmpHRQFuJ7%2FnsG50fmN5JDvdvmBWloB6rjxVWaN4XO6VTWZFZ34JWFyOqgWNEw9aDN3HdsSuJ0Uz19AbdwZBIWe5Elrl71rRJjn1lijCknDB7D4sAmP33k71e%2BB0qvsNl1Shuh9FkY8Z6y05Q%3D%3D"
-    & 7z x flex-2.5.4a-1-lib.zip
-    }
+    appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/win_flex_bison-latest.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1543674503&Signature=CojdaOYrFl50gbxCQL%2BlfVtuo7j9v1OzfWD6jYIkfv1h7xzCacigAM51%2BVjaVx%2B8yvUjk%2B4MOU%2FKmLzev7dABWNi5n7p7SvlXYPFVVwDE57Me35Xi7BzW%2FhoSaPnVIGuhAmDfxjGoHhB0Of%2Fd2FfMl4cklGgc2YafTpFX3agNCE4dcc1UyG0SY5CbvTGTuBP%2B99zaQ69lNT1TSNUNp0PW2Hhj%2FPylts0IdDm713RA4wcNIHvLTTppBiNwMm0y%2B0qRG1op3R4vc5gahz%2B6dTUnCevYWO5l%2FIvmXQyo4XNkgqLKIRgk4wisLjtSuRh5vPyD%2FQPOrn2ubT53YnDcW6geA%3D%3D"
+    7z x win_flex_bison-latest.zip -y
+    Move-Item win_bison.exe bin\bison.exe -force
+    Move-Item win_flex.exe bin\flex.exe -force
+    Move-Item FlexLexer.h include\FlexLexer.h -force
+    Move-Item data bin\data -force
+    bison -V
+    flex -V
     if (!(Test-Path bin\iconv.exe)) {
     & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/libiconv-1.9.2-1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=sS3Y2lC1oWOhBDsL8C9ASuO4LOM%2BpB%2F8PwG5w5CdB9JnPfLqhb3FnA1zkkZJoSNuIYS3DM6CN2qxoWjpJbLEtVQe0PpxziQZjLpJw2MpxXdJiJHRDu8x9THgzwuZ3ze5BWHzPoCBQPdRkKzVPezf1HwptUsm3Y9c2jlWljQjhc8NVsI4iPmjEOwT8E%2BYpR5fsLs2GsRjuoyqKa%2Bi4JJ6MbpXVX1IgR4fzp1Li9SnE39ujHDb%2FyI3c96eCdVm1Oa6jNxzSJNfq%2FgOZM8BIxlR55a%2BtM3oBQhU0voEtDOABwuO7ZBay8dLt%2FG5vz1%2Bi%2FIlRLFxQfICaprPLzw6pXRm8Q%3D%3D"
     & 7z x libiconv-1.9.2-1-bin.zip
 
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc --unwind 5
 ^EXIT=0$
@@ -7,3 +7,6 @@ main.c
 --
 ^warning: ignoring
 ^\[.*<builtin-library-
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -15,3 +15,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -9,3 +9,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10/i;
+        }
+        catch(Exception exc) {
+            assert false;
+        }
+    }
+}
@@ -0,0 +1,4 @@
+package java.lang;
+
+public class ArithmeticException extends RuntimeException {
+}
@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}
@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring
@@ -0,0 +1,11 @@
+public class ArrayIndexOutOfBoundsExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int[] a=new int[4];
+          a[4]=0;
+      }
+      catch (Exception exc) {
+          assert false;
+      }
+  }
+}
@@ -0,0 +1,4 @@
+package java.lang;
+
+public class ArrayIndexOutOfBoundsException extends IndexOutOfBoundsException {
+}
@@ -0,0 +1,4 @@
+package java.lang;
+
+public class IndexOutOfBoundsException extends RuntimeException {
+}