Temporarily disable field-sensitivity for arrays

The Array_Propagation1 test is no longer solved during symex in this
case.

Author: smowton

regression/cbmc-concurrency/struct_and_array1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

regression/cbmc/Array_Propagation1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
@@ -7,3 +7,7 @@ main.c
 (Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
 --
 ^warning: ignoring
+--
+This requires field-sensitive SSA encoding of arrays to pass entirely via
+constant propagation (changing the above condition to "1 remaining after
+simplification" would also make it pass, but this isn't the point of the test).

regression/cbmc/variable-access-to-constant-array/test.desc

@@ -1,4 +1,4 @@
-THOROUGH broken-smt-backend
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
@@ -12,4 +12,4 @@ do so.
 
 Field-sensitive encoding of array accesses for an array of 2^16 elements is very
 expensive. We might consider some bounds up to which we actually do field
-expansion.
+expansion, or at least need to mark this test as "THOROUGH."

src/goto-symex/field_sensitivity.cpp

@@ -16,6 +16,8 @@ Author: Michael Tautschnig
 #include "goto_symex_state.h"
 #include "symex_target.h"
 
+// #define ENABLE_ARRAY_FIELD_SENSITIVITY
+
 void field_sensitivityt::apply(const namespacet &ns, exprt &expr, bool write)
   const
 {
@@ -38,12 +40,14 @@ void field_sensitivityt::apply(const namespacet &ns, exprt &expr, bool write)
   {
     simplify(expr, ns);
   }
+#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     !write && expr.id() == ID_index &&
     to_index_expr(expr).array().id() == ID_array)
   {
     simplify(expr, ns);
   }
+#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_member)
   {
     // turn a member-of-an-SSA-expression into a single SSA expression, thus
@@ -66,6 +70,7 @@ void field_sensitivityt::apply(const namespacet &ns, exprt &expr, bool write)
       expr.swap(tmp);
     }
   }
+#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_index)
   {
     // turn a index-of-an-SSA-expression into a single SSA expression, thus
@@ -89,6 +94,7 @@ void field_sensitivityt::apply(const namespacet &ns, exprt &expr, bool write)
       expr.swap(tmp);
     }
   }
+#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
 }
 
 exprt field_sensitivityt::get_fields(
@@ -115,6 +121,7 @@ exprt field_sensitivityt::get_fields(
 
     return std::move(result);
   }
+#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     ssa_expr.type().id() == ID_array &&
     to_array_type(ssa_expr.type()).size().id() == ID_constant)
@@ -138,6 +145,7 @@ exprt field_sensitivityt::get_fields(
 
     return std::move(result);
   }
+#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else
     return ssa_expr;
 }
@@ -212,6 +220,7 @@ void field_sensitivityt::field_assignments_rec(
       ++fs_it;
     }
   }
+#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(const auto &type = type_try_dynamic_cast<array_typet>(lhs.type()))
   {
     const std::size_t array_size =
@@ -229,6 +238,7 @@ void field_sensitivityt::field_assignments_rec(
       ++fs_it;
     }
   }
+#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(lhs_fs.has_operands())
   {
     PRECONDITION(