From ade0b9c2a827623b7e681c044ca334f894b1e85b Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Wed, 20 Dec 2017 15:42:14 +0000
Subject: [PATCH] Add extra tests for the non-det issue with constants.

---
 regression/goto-instrument/no_nondet_const/main.c    | 8 ++++++++
 regression/goto-instrument/no_nondet_const/test.desc | 8 ++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 regression/goto-instrument/no_nondet_const/main.c
 create mode 100644 regression/goto-instrument/no_nondet_const/test.desc

diff --git a/regression/goto-instrument/no_nondet_const/main.c b/regression/goto-instrument/no_nondet_const/main.c
new file mode 100644
index 00000000000..cc14b26d28a
--- /dev/null
+++ b/regression/goto-instrument/no_nondet_const/main.c
@@ -0,0 +1,8 @@
+int var;
+const int arr[] = {10, 20, 30};
+
+int main(void)
+{
+  var = arr[2];
+  return 0;
+}
diff --git a/regression/goto-instrument/no_nondet_const/test.desc b/regression/goto-instrument/no_nondet_const/test.desc
new file mode 100644
index 00000000000..4056e95e640
--- /dev/null
+++ b/regression/goto-instrument/no_nondet_const/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--nondet-static
+^EXIT=0$
+^SIGNAL=0$
+--
+arr = NONDET\(const signed int \[3ll\]\)
+--