1 files changed, 0 insertions, 44 deletions
diff --git a/test/VectorInstructions/oob-llvm-lt11.c b/test/VectorInstructions/oob-llvm-lt11.c
deleted file mode 100644
index 9d80ef7d..00000000
--- a/test/VectorInstructions/oob-llvm-lt11.c
+++ /dev/null
@@ -1,44 +0,0 @@
-// REQUIRES: lt-llvm-11.0
-// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// NOTE: Have to pass `--optimize=false` to avoid vector operations being
-// constant folded away.
-// RUN: %klee --output-dir=%t.klee-out --optimize=false  %t1.bc > %t.stdout.log 2> %t.stderr.log
-// RUN: FileCheck -input-file=%t.stderr.log %s
-
-#include "klee/klee.h"
-
-#include <assert.h>
-#include <stdint.h>
-#include <stdio.h>
-
-typedef uint32_t v4ui __attribute__((vector_size(16)));
-int main() {
-  v4ui f = {1, 2, 3, 4};
-  int k = klee_range(0, 10, "k");
-
-  if (k == 0) {
-    // CHECK-DAG: [[@LINE+1]]: Out of bounds write when inserting element
-    f[4] = 255; // Out of bounds write
-  }
-
-  if (k == 1) {
-    // CHECK-DAG: [[@LINE+1]]: Out of bounds read when extracting element
-    printf("f[4] = %u\n", f[5]); // Out of bounds
-  }
-
-  if (k > 6) {
-    // Performing read should be ExtractElement instruction.
-    // For now this is an expected limitation.
-    // CHECK-DAG: [[@LINE+1]]: ExtractElement, support for symbolic index not implemented
-    uint32_t readValue = f[k];
-  }
-  else {
-    // Performing write should be InsertElement instructions.
-    // For now this is an expected limitation.
-    // CHECK-DAG: [[@LINE+1]]: InsertElement, support for symbolic index not implemented
-    f[k] = 255;
-  }
-
-  return 0;
-}