ConstantArrayExprVisitor: Fix detection of multiple array indices

Previously, the code did two consecutive checks.  First one succeeded
only if the given index was not already seen and the second one did
an analogous check but for arrays.  However, if the given index usage
was already detected for some array, its usage for another array that
already had some other index detected would be silently skipped and the
`incompatible` flag would not be set.

Therefore, if the code contained e.g. the following conditional jump on two
arrays with two symbolic indices, the multi-index access would remain
undetected:

if ((array1[k] + array2[x] + array2[k]) == 0)

Resulting in the following output:

KLEE: WARNING: OPT_I: infeasible branch!
KLEE: WARNING: OPT_I: successful

3 files changed, 55 insertions, 13 deletions

diff --git a/include/klee/Expr/ArrayExprVisitor.h b/include/klee/Expr/ArrayExprVisitor.h
index 28f485d9..b2941e42 100644
--- a/include/klee/Expr/ArrayExprVisitor.h
+++ b/include/klee/Expr/ArrayExprVisitor.h
@@ -35,8 +35,6 @@ class ConstantArrayExprVisitor : public ExprVisitor {
 private:
   using bindings_ty = std::map<const Array *, std::vector<ref<Expr>>>;
   bindings_ty &arrays;
-  // Avoids adding the same index twice
-  std::unordered_set<unsigned> addedIndexes;
   bool incompatible;
 
 protected:
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index 0965308a..cf0da7f6 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -73,18 +73,16 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) {
     }
     IndexCompatibilityExprVisitor compatible;
     compatible.visit(re.index);
-    if (compatible.isCompatible() &&
-        addedIndexes.find(re.index.get()->hash()) == addedIndexes.end()) {
-      if (arrays.find(re.updates.root) == arrays.end()) {
-        arrays.insert(
-            std::make_pair(re.updates.root, std::vector<ref<Expr> >()));
-      } else {
-        // Another possible index to resolve, currently unsupported
-        incompatible = true;
-        return Action::skipChildren();
+    if (compatible.isCompatible()) {
+      if (arrays.count(re.updates.root) > 0) {
+        const auto &indices = arrays[re.updates.root];
+        if (!indices.empty() && indices.front() != re.index) {
+          // Another possible index to resolve, currently unsupported
+          incompatible = true;
+          return Action::skipChildren();
+        }
       }
-      arrays.find(re.updates.root)->second.push_back(re.index);
-      addedIndexes.insert(re.index.get()->hash());
+      arrays[re.updates.root].push_back(re.index);
     } else if (compatible.hasInnerReads()) {
       // This Read has an inner Read, we want to optimize the inner one
       // to create a cascading effect during assignment evaluation
diff --git a/test/ArrayOpt/test_multindex_multarray.c b/test/ArrayOpt/test_multindex_multarray.c
new file mode 100644
index 00000000..54e91f48
--- /dev/null
+++ b/test/ArrayOpt/test_multindex_multarray.c
@@ -0,0 +1,46 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=index %t.bc > %t.log 2>&1
+// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+
+// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
+// CHECK-CONST_ARR: const_arr
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+char array1[5] = {0, 1, 2, 3, 4};
+char array2[5] = {0, 1, 2, 3, 4};
+
+int main() {
+  unsigned k;
+  unsigned x;
+
+  klee_make_symbolic(&k, sizeof(k), "k");
+  klee_assume(k < 5);
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_assume(x < 5);
+
+  // CHECK: Yes
+  if ((array1[k] + array2[x] + array2[k]) - 7 == 0)
+    printf("Yes\n");
+
+  // CHECK: KLEE: done: completed paths = 2
+
+  return 0;
+}