1 files changed, 18 insertions, 0 deletions
diff --git a/test/regression/2007-07-30-unflushed-byte.c b/test/regression/2007-07-30-unflushed-byte.c
new file mode 100644
index 00000000..ba8a08a7
--- /dev/null
+++ b/test/regression/2007-07-30-unflushed-byte.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+
+#include <assert.h>
+
+int main() {
+  char i, x[3];
+
+  klee_make_symbolic(&i, sizeof i);
+
+  x[0] = i;
+
+  // DEMAND FAILED:Memory.cpp:read8:199: <isByteFlushed(offset)> is false: "unflushed byte without cache value"
+  char y =  x[1];
+
+  return 0;
+}
+