Add failing test for the ignore-before-unwind option

to be fixed, but until then, marked as KNOWBUG.

Author: petr-bauch

regression/cbmc-incr-oneloop/ignore-before-unwind/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  __CPROVER_bool assumption = (__CPROVER_bool)0;
+  __CPROVER_bool property = (__CPROVER_bool)1;
+
+  while(1)
+  {
+    __CPROVER_assume(property == 1);
+    assumption = 1;
+    property = 0;
+    __CPROVER_assert(property == 1, "property");
+  }
+  return 0;
+}

regression/cbmc-incr-oneloop/ignore-before-unwind/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--ignore-properties-before-unwind-min --incremental-loop main.0 --no-unwinding-assertions --max-node-refinement 1 --unwind-max 2
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ property: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring