Fix ignoring properties before unwind min (off-by-one)

Basically, if unwind-min is zero (by default) the first loop iterations should
not be ignored (even if requested). Tests show the problem.

Author: petr-bauch

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

@@ -0,0 +1,12 @@
+CORE
+main.c
+--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ property: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This test correctly fails because the first iteration of the loop violates the
+property.

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

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

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test "correctly" succeeds because the second iteration of the loop is
+unreachable due to the assumption which is violated after the first iteration.
+This behaviour is intended and documented, i.e. using ignore-before-unwind
+assumes that we know that iterations before unwind-min are correct.

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -36,6 +36,7 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
                                    : 0)
 {
   ignore_assertions =
+    incr_min_unwind >= 1 &&
     options.get_bool_option("ignore-properties-before-unwind-min");
 }