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/andNot_Pass.class

@@ -0,0 +1,8 @@
+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
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+--

jbmc/regression/jbmc/nondet_propagation1/andNot_Pass.desc

@@ -0,0 +1,40 @@
+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));
+  }
+}