diff --git a/c/check.py b/c/check.py
index e7900454988..f48f4e7da71 100755
--- a/c/check.py
+++ b/c/check.py
@@ -122,6 +122,7 @@
     ("loop-lit", "gcnr2008_false-unreach-call_false-termination.c is not contained in any category"),
     ("recursive", "Addition03_false-no-overflow.c is not contained in any category"),
     ("ssh-simplified", "s3_clnt_3.cil_true-unreach-call_true-termination.c is not contained in any category"),
+    ("termination-crafted", "Nyala-2lex_false-valid-deref.c is not contained in any category"),
     ("termination-memory-alloca", "cll_by_lseg-alloca_false-termination.c is not contained in any category"),
     ("termination-memory-alloca", "cll_by_lseg-alloca_true-termination.c is not contained in any category"),
     ("termination-memory-alloca", "cll_by_lseg_traverse-alloca_false-termination.c is not contained in any category"),
diff --git a/c/termination-crafted/Nyala-2lex_false-valid-deref.c b/c/termination-crafted/Nyala-2lex_false-valid-deref.c
new file mode 100755
index 00000000000..f210b34094f
--- /dev/null
+++ b/c/termination-crafted/Nyala-2lex_false-valid-deref.c
@@ -0,0 +1,25 @@
+/*
+ * Date: 2013-07-13
+ * Author: leike@informatik.uni-freiburg.de
+ *
+ * Simple test case for the lexicographic template.
+ * Has the lexicographic ranking function
+ * f(x, y) = <x, y>
+ *
+ */
+
+typedef enum {false, true} bool;
+
+extern int __VERIFIER_nondet_int(void);
+
+int main() {
+	int x, y;
+	while (x >= 0 && y >= 0) {
+		y = y - 1;
+		if (y < 0) {
+			x = x - 1;
+			y = __VERIFIER_nondet_int();
+		}
+	}
+    return 0;
+}