From db3aa790007b6bc1d97d1a46079fd03a77d82f0b Mon Sep 17 00:00:00 2001
From: Michael Emmi <michael.emmi@gmail.com>
Date: Tue, 18 Mar 2014 10:08:58 +0100
Subject: [PATCH] Added another failing example. * pointers to separate regions
 should be unequal.

---
 examples/failing/extern_mem2.c | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 examples/failing/extern_mem2.c

diff --git a/examples/failing/extern_mem2.c b/examples/failing/extern_mem2.c
new file mode 100644
index 000000000..75b8abe6b
--- /dev/null
+++ b/examples/failing/extern_mem2.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+#include <smack.h>
+
+void foo(int*);
+int* bar();
+
+int main() {
+  int *x = malloc(4);
+  int *y = malloc(4);
+  int *z;
+
+  foo(y);
+  z = bar();
+
+  *x = 1;
+  *z = 2;
+
+  __SMACK_assert(x != z);
+}
\ No newline at end of file