Add negation tests for array equal

This ensures the condition doesn't introduce too strong constraints

Author: Thomas Kiley

regression/cbmc/Array_operations1/main.c

@@ -19,6 +19,7 @@ void test_unequal()
 
   __CPROVER_assert(
     !__CPROVER_array_equal(a1, a2), "different sizes arrays are unequal");
+  __CPROVER_assert(__CPROVER_array_equal(a1, a2), "expected to fail");
 
   float a3[10];
   void *lost_type1 = a1;
@@ -27,6 +28,15 @@ void test_unequal()
   __CPROVER_assert(
     !__CPROVER_array_equal(lost_type1, lost_type3),
     "different typed arrays are unequal");
+  __CPROVER_assert(
+    __CPROVER_array_equal(lost_type1, lost_type3), "expected to fail");
+
+  int a4[10];
+  int a5[10];
+
+  // Here the arrays both can be equal, and be not equal, so both asserts should fail
+  __CPROVER_assert(!__CPROVER_array_equal(a4, a5), "expected to fail");
+  __CPROVER_assert(__CPROVER_array_equal(a4, a5), "expected to fail");
 }
 
 void test_copy()

regression/cbmc/Array_operations1/test.desc

@@ -5,8 +5,12 @@ main.c
 ^SIGNAL=0$
 ^\[test_copy\.assertion\.4\] .* expected to fail: FAILURE$
 ^\[test_unequal\.assertion\.1\] .* different sizes arrays are unequal: SUCCESS
-^\[test_unequal\.assertion\.2\] .* different typed arrays are unequal: SUCCESS
-^\*\* 1 of 10 failed
+^\[test_unequal\.assertion\.2\] .* expected to fail: FAILURE
+^\[test_unequal\.assertion\.3\] .* different typed arrays are unequal: SUCCESS
+^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
+^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
+^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
+^\*\* 5 of 14 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring