Revert "Removed duplicate benchmark"

This reverts commit 9182d44.
sosy-lab · Nov 27, 2016 · 85a695e · 85a695e · dbeyer · Nov 27, 2016
1 parent a984fe7
commit 85a695e
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 0 deletions.
diff --git 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
@@ -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;
+}