Additional unbounded-array test that should continue to pass

This test passes without nondet-propagation, and should continue to pass
if/when it is merged.

Author: tautschnig

jbmc/regression/jbmc/nondet_propagation1/BitSet.class

@@ -0,0 +1,10 @@
+CORE
+andNot_Pass.class
+--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100 --function andNot_Pass.main
+^\[java::andNot_Pass\.main:\(\[Ljava/lang/String;\)V.assertion\.3\] line 40 assertion at file andNot_Pass\.java line 40 function java::andNot_Pass.main:\(\[Ljava/lang/String;\)V bytecode-index 52: FAILURE$
+^\*\* 1 of \d+ failed
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/nondet_propagation1/andNot_Pass.class

@@ -0,0 +1,42 @@
+class BitSet {
+  boolean bits[];
+  public BitSet()
+  {
+    int size = org.cprover.CProver.nondetInt();
+    org.cprover.CProver.assume(size >= 0);
+    bits = new boolean[size];
+  }
+  public void set(int i)
+  {
+    org.cprover.CProver.assume(i < bits.length);
+    bits[i] = true;
+  }
+  public boolean get(int i)
+  {
+    if(i < bits.length)
+      return bits[i];
+    return false;
+  }
+  public void andNot(BitSet other)
+  {
+    for (int i = 0; i < bits.length; i++) {
+      bits[i] = bits[i] && !other.get(i);
+    }
+  }
+}
+
+public class andNot_Pass {
+  public static void main(String args[]) {
+    BitSet b1 = new BitSet();
+    b1.set(1);
+    b1.set(2);
+    BitSet b2 = new BitSet();
+    b2.set(0);
+    b2.set(2);
+    b1.andNot(b2);
+
+    assert(!b1.get(0));
+    assert(b1.get(1));
+    assert(b1.get(2)); // expected to fail
+  }
+}