diff --git a/verification/verifast/problems/README.md b/verification/verifast/problems/README.md
new file mode 100644
index 000000000..712ec2815
--- /dev/null
+++ b/verification/verifast/problems/README.md
@@ -0,0 +1,2 @@
+This directory contains collection of problems encountered with VeriFast that
+need to be fixed in order to verify the current code base as is.
diff --git a/verification/verifast/problems/bugs/define_name/defining_header.h b/verification/verifast/problems/bugs/define_name/defining_header.h
new file mode 100644
index 000000000..e63adcfa0
--- /dev/null
+++ b/verification/verifast/problems/bugs/define_name/defining_header.h
@@ -0,0 +1,10 @@
+#define ABC
+
+
+/*
+#ifdef ABC				// ok: evaluates to true
+    #error "ABC defined"		
+#else					// ok: evaluates to false
+    #error "ABC not defined"
+#endif
+*/
diff --git a/verification/verifast/problems/bugs/define_name/main.c b/verification/verifast/problems/bugs/define_name/main.c
new file mode 100644
index 000000000..c71f3ef2f
--- /dev/null
+++ b/verification/verifast/problems/bugs/define_name/main.c
@@ -0,0 +1,20 @@
+/* Bug:
+ * The header `defining_header.h` defines the constant `ABC` and
+ * the header `testing_header.h` checks whether `ABC` has been defined.
+ * In `testing_header.h` both checks `#ifdef ABC` and its negation
+ * `#ifndef ABC` evaluate to true.
+ */
+
+#include "defining_header.h"
+
+
+/*
+#ifdef ABC			// ok: evaluates to true
+    #error "ABC defined"		
+#else				// ok: evaluates to false
+    #error "ABC not defined"
+#endif
+*/
+
+
+#include "testing_header.h"
\ No newline at end of file
diff --git a/verification/verifast/problems/bugs/define_name/testing_header.h b/verification/verifast/problems/bugs/define_name/testing_header.h
new file mode 100644
index 000000000..9add91a69
--- /dev/null
+++ b/verification/verifast/problems/bugs/define_name/testing_header.h
@@ -0,0 +1,17 @@
+// Problem: Both branches branch conditions evaluate to true.
+
+/* `main.c` included this header after including `defining_header.h`.
+ * Hence, `#ifdef ABC` should evaluate to true and `#ifndef ABC should
+ * evaluate to false.
+ */
+
+/*
+#ifdef ABC			// ok: evaluates to true.
+    #error "ABC defined"	
+#endif
+*/
+
+
+#ifndef ABC			// bug: evaluates to true
+    #error "ABC defined"
+#endif
\ No newline at end of file