Add cbmc --incremental regression tests as FUTURE

We have these tests in the repository, but did not include them in
either Makefile or CMake configurations. They can't work right now as
the "--incremental" command-line option doesn't yet exist, thus marking
them as "FUTURE."

Author: tautschnig

regression/CMakeLists.txt

@@ -32,6 +32,9 @@ add_subdirectory(cpp)
 add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
+add_subdirectory(cbmc-incr)
+add_subdirectory(cbmc-with-incr)
+add_subdirectory(array-refinement-with-incr)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)
 add_subdirectory(smt2_strings)

regression/Makefile

@@ -10,6 +10,9 @@ DIRS = cbmc \
        cbmc-concurrency \
        cbmc-cover \
        cbmc-incr-oneloop \
+       cbmc-incr \
+       cbmc-with-incr \
+       array-refinement-with-incr \
        goto-instrument-typedef \
        smt2_solver \
        smt2_strings \

regression/array-refinement-with-incr/Array_UF1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF10/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF11/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF12/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF13/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF14/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 6
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF15/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF16/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$