From 4189407d5c96f6672de5582cb97df48084337841 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@cs.ox.ac.uk>
Date: Sat, 18 Jun 2016 16:15:36 +0100
Subject: [PATCH] run datastax removed

---
 regression/run-datastax.sh | 13 -------------
 1 file changed, 13 deletions(-)
 delete mode 100755 regression/run-datastax.sh

diff --git a/regression/run-datastax.sh b/regression/run-datastax.sh
deleted file mode 100755
index 793be5a9097..00000000000
--- a/regression/run-datastax.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-#!/bin/bash
-test_cases=`find cbmc-java/datastax/ -name *.desc -exec dirname {} \;`
-./test.pl -c $1 ${test_cases}
-
-count=0
-for test_case in ${test_cases}; do
-  out_file=`find ${test_case} -name '*.out'`
-  if grep -q "identifier.*not found" ${out_file}; then
-    echo ${out_file}
-    count=$((${count}+1))
-  fi
-done;
-echo "Missing symbols: ${count}"