Fix array constraints for with_exprt with >3 operands

The initial support for more than 3 operands in 02e508e generated possibly
inconsistent constraints. Also update comments to describe multiple update
operands.

The test is based on SV-COMP's array-memsafety/count_down_unsafe_false-valid-deref.c.

Author: tautschnig

regression/cbmc/array_constraints1/main.c

@@ -0,0 +1,32 @@
+#include <stdlib.h>
+
+extern int __VERIFIER_nondet_int(void);
+
+int main()
+{
+  int i, j;
+  int val;
+  int length = __VERIFIER_nondet_int();
+  if(length < 1)
+    length = 1;
+  int *arr = malloc(length);
+  if(!arr)
+    return 0;
+  for(i = 0; i < length; i++)
+  {
+    val = __VERIFIER_nondet_int();
+    if(val < 0)
+    {
+      val = 0;
+    }
+    arr[i] = val;
+  }
+  for(j = 0; j < length; j++)
+  {
+    while(arr[j] > 0)
+    {
+      arr[j]--;
+    }
+  }
+  return 0;
+}

regression/cbmc/array_constraints1/test.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+main.c
+--unwind 2 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 2 of 14
+--
+^warning: ignoring

src/solvers/flattening/arrays.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
+#include <unordered_set>
+
 arrayst::arrayst(const namespacet &_ns, propt &_prop)
   : equalityt(_prop), ns(_ns)
 {
@@ -505,21 +507,16 @@ void arrayst::add_array_constraints_with(
   const index_sett &index_set,
   const with_exprt &expr)
 {
+  // We got x=(y with [i:=v, j:=w, ...]).
+  // First add constraints x[i]=v, x[j]=w, ...
+  std::unordered_set<exprt, irep_hash> updated_indices;
+
   const exprt::operandst &operands = expr.operands();
   for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
-    add_array_constraints_with(index_set, expr, operands[i], operands[i + 1]);
-}
-
-void arrayst::add_array_constraints_with(
-  const index_sett &index_set,
-  const with_exprt &expr,
-  const exprt &index,
-  const exprt &value)
-{
-  // we got x=(y with [i:=v])
-  // add constraint x[i]=v
-
   {
+    const exprt &index = operands[i];
+    const exprt &value = operands[i + 1];
+
     index_exprt index_expr(expr, index, expr.type().subtype());
 
     if(index_expr.type()!=value.type())
@@ -531,22 +528,29 @@ void arrayst::add_array_constraints_with(
     }
 
     lazy_constraintt lazy(
-       lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
-     add_array_constraint(lazy, false); // added immediately
+      lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
+    add_array_constraint(lazy, false); // added immediately
+
+    updated_indices.insert(index);
   }
 
-  // use other array index applications for "else" case
-  // add constraint x[I]=y[I] for I!=i
+  // For all other indices use the existing value, i.e., add constraints
+  // x[I]=y[I] for I!=i,j,...
 
   for(auto other_index : index_set)
   {
-    if(other_index!=index)
+    if(updated_indices.find(other_index) == updated_indices.end())
     {
       // we first build the guard
+      exprt::operandst disjuncts;
+      disjuncts.reserve(updated_indices.size());
+      for(const auto &index : updated_indices)
+      {
+        disjuncts.push_back(equal_exprt{
+          index, typecast_exprt::conditional_cast(other_index, index.type())});
+      }
 
-      other_index = typecast_exprt::conditional_cast(other_index, index.type());
-
-      literalt guard_lit=convert(equal_exprt(index, other_index));
+      literalt guard_lit = convert(disjunction(disjuncts));
 
       if(guard_lit!=const_literal(true))
       {

src/solvers/flattening/arrays.h

@@ -111,11 +111,6 @@ class arrayst:public equalityt
     const index_sett &index_set, const if_exprt &exprt);
   void add_array_constraints_with(
     const index_sett &index_set, const with_exprt &expr);
-  void add_array_constraints_with(
-    const index_sett &index_set,
-    const with_exprt &expr,
-    const exprt &index,
-    const exprt &value);
   void add_array_constraints_update(
     const index_sett &index_set, const update_exprt &expr);
   void add_array_constraints_array_of(