Ignore properties before unwind min

Allows to check assertions only between unwind-min and unwind-max
iterations of a specified loop.

Author: peterschrammel

regression/cbmc-incr-oneloop/minmaxunwind4/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
---unwind-min 6 --unwind-max 8 --incremental-loop main.0
+--unwind-min 6 --unwind-max 8 --incremental-loop main.0 --ignore-properties-before-unwind-min
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+^Generated 1 VCC\(s\), \d+ remaining after simplification$
 --
+^Generated 6 VCC\(s\), \d+ remaining after simplification$
 ^warning: ignoring

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -35,6 +35,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
       options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min")
                                    : 0)
 {
+  ignore_assertions =
+    options.get_bool_option("ignore-properties-before-unwind-min");
 }
 
 bool symex_bmc_incremental_one_loopt::should_stop_unwind(