diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index c8b8382526f..911f4e0f014 100644 --- a/regression/CMakeLists.txt +++ b/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) diff --git a/regression/Makefile b/regression/Makefile index 9cc13313e34..f5cda758189 100644 --- a/regression/Makefile +++ b/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 \ diff --git a/regression/array-refinement-with-incr/Array_UF1/test.desc b/regression/array-refinement-with-incr/Array_UF1/test.desc index 3fccfdb3d33..b5f97a1c26f 100644 --- a/regression/array-refinement-with-incr/Array_UF1/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF10/test.desc b/regression/array-refinement-with-incr/Array_UF10/test.desc index a8467ba9016..bd5ad60bd91 100644 --- a/regression/array-refinement-with-incr/Array_UF10/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF11/test.desc b/regression/array-refinement-with-incr/Array_UF11/test.desc index 6629a4524e7..878da0a41b5 100644 --- a/regression/array-refinement-with-incr/Array_UF11/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF12/test.desc b/regression/array-refinement-with-incr/Array_UF12/test.desc index 5cc1222bf70..bd65d053b3d 100644 --- a/regression/array-refinement-with-incr/Array_UF12/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF13/test.desc b/regression/array-refinement-with-incr/Array_UF13/test.desc index a8467ba9016..bd5ad60bd91 100644 --- a/regression/array-refinement-with-incr/Array_UF13/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF14/test.desc b/regression/array-refinement-with-incr/Array_UF14/test.desc index ec5e788bd97..9e500d61b9d 100644 --- a/regression/array-refinement-with-incr/Array_UF14/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF15/test.desc b/regression/array-refinement-with-incr/Array_UF15/test.desc index 3fccfdb3d33..b5f97a1c26f 100644 --- a/regression/array-refinement-with-incr/Array_UF15/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF16/test.desc b/regression/array-refinement-with-incr/Array_UF16/test.desc index 5cc1222bf70..bd65d053b3d 100644 --- a/regression/array-refinement-with-incr/Array_UF16/test.desc +++ b/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$ diff --git a/regression/array-refinement-with-incr/Array_UF17/test.desc b/regression/array-refinement-with-incr/Array_UF17/test.desc index fa1ab28a768..782725838bb 100644 --- a/regression/array-refinement-with-incr/Array_UF17/test.desc +++ b/regression/array-refinement-with-incr/Array_UF17/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 9 ^EXIT=0$ diff --git a/regression/array-refinement-with-incr/Array_UF18/test.desc b/regression/array-refinement-with-incr/Array_UF18/test.desc index 3fccfdb3d33..b5f97a1c26f 100644 --- a/regression/array-refinement-with-incr/Array_UF18/test.desc +++ b/regression/array-refinement-with-incr/Array_UF18/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 11 ^EXIT=0$ diff --git a/regression/array-refinement-with-incr/Array_UF19/test.desc b/regression/array-refinement-with-incr/Array_UF19/test.desc index 4acc3fa7050..29f4fdc1b61 100644 --- a/regression/array-refinement-with-incr/Array_UF19/test.desc +++ b/regression/array-refinement-with-incr/Array_UF19/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 3 ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/Array_UF2/test.desc b/regression/array-refinement-with-incr/Array_UF2/test.desc index 80b8d99475e..fdab757dc1a 100644 --- a/regression/array-refinement-with-incr/Array_UF2/test.desc +++ b/regression/array-refinement-with-incr/Array_UF2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 5 ^EXIT=0$ diff --git a/regression/array-refinement-with-incr/Array_UF20/test.desc b/regression/array-refinement-with-incr/Array_UF20/test.desc index 11a7b0213c5..708a3418119 100644 --- a/regression/array-refinement-with-incr/Array_UF20/test.desc +++ b/regression/array-refinement-with-incr/Array_UF20/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 12 ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/Array_UF3/test.desc b/regression/array-refinement-with-incr/Array_UF3/test.desc index 4a6354151db..914f7253e42 100644 --- a/regression/array-refinement-with-incr/Array_UF3/test.desc +++ b/regression/array-refinement-with-incr/Array_UF3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 3 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/Array_UF4/test.desc b/regression/array-refinement-with-incr/Array_UF4/test.desc index d7d2fb825e7..c8ca724650f 100644 --- a/regression/array-refinement-with-incr/Array_UF4/test.desc +++ b/regression/array-refinement-with-incr/Array_UF4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 2 ^EXIT=0$ diff --git a/regression/array-refinement-with-incr/Array_UF5/test.desc b/regression/array-refinement-with-incr/Array_UF5/test.desc index 5cc1222bf70..bd65d053b3d 100644 --- a/regression/array-refinement-with-incr/Array_UF5/test.desc +++ b/regression/array-refinement-with-incr/Array_UF5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 2 ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/Array_UF6/test.desc b/regression/array-refinement-with-incr/Array_UF6/test.desc index 4acc3fa7050..29f4fdc1b61 100644 --- a/regression/array-refinement-with-incr/Array_UF6/test.desc +++ b/regression/array-refinement-with-incr/Array_UF6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 3 ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/Array_UF7/test.desc b/regression/array-refinement-with-incr/Array_UF7/test.desc index 4acc3fa7050..29f4fdc1b61 100644 --- a/regression/array-refinement-with-incr/Array_UF7/test.desc +++ b/regression/array-refinement-with-incr/Array_UF7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 3 ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/Array_UF8/test.desc b/regression/array-refinement-with-incr/Array_UF8/test.desc index efa322956fc..8ddd09029a6 100644 --- a/regression/array-refinement-with-incr/Array_UF8/test.desc +++ b/regression/array-refinement-with-incr/Array_UF8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 6 ^EXIT=0$ diff --git a/regression/array-refinement-with-incr/Array_UF9/test.desc b/regression/array-refinement-with-incr/Array_UF9/test.desc index b786bf61e5f..b756d46f954 100644 --- a/regression/array-refinement-with-incr/Array_UF9/test.desc +++ b/regression/array-refinement-with-incr/Array_UF9/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --arrays-uf-always --no-propagation --unwind-max 21 ^EXIT=10$ diff --git a/regression/array-refinement-with-incr/CMakeLists.txt b/regression/array-refinement-with-incr/CMakeLists.txt new file mode 100644 index 00000000000..da7f7e70da7 --- /dev/null +++ b/regression/array-refinement-with-incr/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$ --incremental" +) diff --git a/regression/cbmc-incr/Ackermann02_false1/test.desc b/regression/cbmc-incr/Ackermann02_false1/test.desc index feb208278d1..fe5e0b6d27c 100644 --- a/regression/cbmc-incr/Ackermann02_false1/test.desc +++ b/regression/cbmc-incr/Ackermann02_false1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR --unwind-max 6 ^EXIT=10$ diff --git a/regression/cbmc-incr/MultCommutative_true1/test.desc b/regression/cbmc-incr/MultCommutative_true1/test.desc index a907bb6415d..3e307e571fe 100644 --- a/regression/cbmc-incr/MultCommutative_true1/test.desc +++ b/regression/cbmc-incr/MultCommutative_true1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR --unwind-max 6 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/alarm1/test.desc b/regression/cbmc-incr/alarm1/test.desc index 0b88cadbc06..650d3b27961 100644 --- a/regression/cbmc-incr/alarm1/test.desc +++ b/regression/cbmc-incr/alarm1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 25 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/alarm2/test.desc b/regression/cbmc-incr/alarm2/test.desc index 0d034169229..f51d0255b05 100644 --- a/regression/cbmc-incr/alarm2/test.desc +++ b/regression/cbmc-incr/alarm2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-min 5 --unwind-max 10 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc-incr/alarm3/test.desc b/regression/cbmc-incr/alarm3/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/alarm3/test.desc +++ b/regression/cbmc-incr/alarm3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/arrays2/test.desc b/regression/cbmc-incr/arrays2/test.desc index ace61c7fe7b..66f3d0a2450 100644 --- a/regression/cbmc-incr/arrays2/test.desc +++ b/regression/cbmc-incr/arrays2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 5 --no-unwinding-assertions --arrays-uf-always ^EXIT=10$ diff --git a/regression/cbmc-incr/arrays3/test.desc b/regression/cbmc-incr/arrays3/test.desc index e811d53f304..3beceac1239 100644 --- a/regression/cbmc-incr/arrays3/test.desc +++ b/regression/cbmc-incr/arrays3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/arrays4/test.desc b/regression/cbmc-incr/arrays4/test.desc index e811d53f304..3beceac1239 100644 --- a/regression/cbmc-incr/arrays4/test.desc +++ b/regression/cbmc-incr/arrays4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/arrays5/test.desc b/regression/cbmc-incr/arrays5/test.desc index c7aedd490fb..67c1665c96d 100644 --- a/regression/cbmc-incr/arrays5/test.desc +++ b/regression/cbmc-incr/arrays5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 5 --no-unwinding-assertions --arrays-uf-always ^EXIT=0$ diff --git a/regression/cbmc-incr/assertion-after-loop1/test.desc b/regression/cbmc-incr/assertion-after-loop1/test.desc index 3ede5ed0f72..efb176e1ccc 100644 --- a/regression/cbmc-incr/assertion-after-loop1/test.desc +++ b/regression/cbmc-incr/assertion-after-loop1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 10 ^EXIT=10$ diff --git a/regression/cbmc-incr/assertion-after-loop2/test.desc b/regression/cbmc-incr/assertion-after-loop2/test.desc index 7a617d1973c..f17855ff1c8 100644 --- a/regression/cbmc-incr/assertion-after-loop2/test.desc +++ b/regression/cbmc-incr/assertion-after-loop2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-max 10 ^EXIT=0$ diff --git a/regression/cbmc-incr/cruise1/test.desc b/regression/cbmc-incr/cruise1/test.desc index 9474865a7c9..1a489aaeeff 100644 --- a/regression/cbmc-incr/cruise1/test.desc +++ b/regression/cbmc-incr/cruise1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 10 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/cruise2/test.desc b/regression/cbmc-incr/cruise2/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/cruise2/test.desc +++ b/regression/cbmc-incr/cruise2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/email_spec27_product31_false1/test.desc b/regression/cbmc-incr/email_spec27_product31_false1/test.desc index edff8ba88f3..beb86c48175 100644 --- a/regression/cbmc-incr/email_spec27_product31_false1/test.desc +++ b/regression/cbmc-incr/email_spec27_product31_false1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR --unwind-max 3 ^EXIT=10$ diff --git a/regression/cbmc-incr/induction1/test.desc b/regression/cbmc-incr/induction1/test.desc index 0f773f9e2ab..5b28f0ad371 100644 --- a/regression/cbmc-incr/induction1/test.desc +++ b/regression/cbmc-incr/induction1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --stop-when-unsat --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/magic1/test.desc b/regression/cbmc-incr/magic1/test.desc index d723f0ec32e..44dc9051110 100644 --- a/regression/cbmc-incr/magic1/test.desc +++ b/regression/cbmc-incr/magic1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --magic-numbers ^EXIT=0$ diff --git a/regression/cbmc-incr/minmaxunwind1/test.desc b/regression/cbmc-incr/minmaxunwind1/test.desc index 5c9b0241320..32f77897568 100644 --- a/regression/cbmc-incr/minmaxunwind1/test.desc +++ b/regression/cbmc-incr/minmaxunwind1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-min 4 --unwind-max 6 ^EXIT=10$ diff --git a/regression/cbmc-incr/minmaxunwind2/test.desc b/regression/cbmc-incr/minmaxunwind2/test.desc index 0626ccb6645..1e5dc911cc5 100644 --- a/regression/cbmc-incr/minmaxunwind2/test.desc +++ b/regression/cbmc-incr/minmaxunwind2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-min 5 --unwind-max 5 ^EXIT=10$ diff --git a/regression/cbmc-incr/minmaxunwind3/test.desc b/regression/cbmc-incr/minmaxunwind3/test.desc index 112bb920bdd..b9e907489b8 100644 --- a/regression/cbmc-incr/minmaxunwind3/test.desc +++ b/regression/cbmc-incr/minmaxunwind3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-min 2 --unwind-max 4 ^EXIT=0$ diff --git a/regression/cbmc-incr/minmaxunwind4/test.desc b/regression/cbmc-incr/minmaxunwind4/test.desc index b1c035a6005..e3a5007d81d 100644 --- a/regression/cbmc-incr/minmaxunwind4/test.desc +++ b/regression/cbmc-incr/minmaxunwind4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-min 6 --unwind-max 8 ^EXIT=10$ diff --git a/regression/cbmc-incr/minmaxunwind5/test.desc b/regression/cbmc-incr/minmaxunwind5/test.desc index 337f56ebade..4b81055826f 100644 --- a/regression/cbmc-incr/minmaxunwind5/test.desc +++ b/regression/cbmc-incr/minmaxunwind5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-min 4 ^EXIT=10$ diff --git a/regression/cbmc-incr/moreasserts1/test.desc b/regression/cbmc-incr/moreasserts1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/moreasserts1/test.desc +++ b/regression/cbmc-incr/moreasserts1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/moreloops1/test.desc b/regression/cbmc-incr/moreloops1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/moreloops1/test.desc +++ b/regression/cbmc-incr/moreloops1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/nestedloop1/test.desc b/regression/cbmc-incr/nestedloop1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/nestedloop1/test.desc +++ b/regression/cbmc-incr/nestedloop1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/no-unwinding-assertion1/test.desc b/regression/cbmc-incr/no-unwinding-assertion1/test.desc index 7a617d1973c..f17855ff1c8 100644 --- a/regression/cbmc-incr/no-unwinding-assertion1/test.desc +++ b/regression/cbmc-incr/no-unwinding-assertion1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-max 10 ^EXIT=0$ diff --git a/regression/cbmc-incr/recursion1/test.desc b/regression/cbmc-incr/recursion1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-incr/recursion1/test.desc +++ b/regression/cbmc-incr/recursion1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-incr/recursion2/test.desc b/regression/cbmc-incr/recursion2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-incr/recursion2/test.desc +++ b/regression/cbmc-incr/recursion2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-incr/simpleloop1/test.desc b/regression/cbmc-incr/simpleloop1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/simpleloop1/test.desc +++ b/regression/cbmc-incr/simpleloop1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/simpleloop2/test.desc b/regression/cbmc-incr/simpleloop2/test.desc index eb832bc4041..acae2360065 100644 --- a/regression/cbmc-incr/simpleloop2/test.desc +++ b/regression/cbmc-incr/simpleloop2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 6 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc-incr/simpleloop3/test.desc b/regression/cbmc-incr/simpleloop3/test.desc index 9b667e07606..1ad8506ebe7 100644 --- a/regression/cbmc-incr/simpleloop3/test.desc +++ b/regression/cbmc-incr/simpleloop3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc-incr/simpleloopmax1/test.desc b/regression/cbmc-incr/simpleloopmax1/test.desc index 4b23aaa8a1e..dc32e82ea45 100644 --- a/regression/cbmc-incr/simpleloopmax1/test.desc +++ b/regression/cbmc-incr/simpleloopmax1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-max 10 ^EXIT=10$ diff --git a/regression/cbmc-incr/simpleloopmax2/test.desc b/regression/cbmc-incr/simpleloopmax2/test.desc index 7a617d1973c..f17855ff1c8 100644 --- a/regression/cbmc-incr/simpleloopmax2/test.desc +++ b/regression/cbmc-incr/simpleloopmax2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-unwinding-assertions --unwind-max 10 ^EXIT=0$ diff --git a/regression/cbmc-incr/simplifier1/test.desc b/regression/cbmc-incr/simplifier1/test.desc index d4fd36300ef..e4ee9f7fc38 100644 --- a/regression/cbmc-incr/simplifier1/test.desc +++ b/regression/cbmc-incr/simplifier1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 5 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/simplifier2/test.desc b/regression/cbmc-incr/simplifier2/test.desc index bcf28728cec..41bba6f99c4 100644 --- a/regression/cbmc-incr/simplifier2/test.desc +++ b/regression/cbmc-incr/simplifier2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 3 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/simplifier3/test.desc b/regression/cbmc-incr/simplifier3/test.desc index d4fd36300ef..e4ee9f7fc38 100644 --- a/regression/cbmc-incr/simplifier3/test.desc +++ b/regression/cbmc-incr/simplifier3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 5 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/sum_array_true1/test.desc b/regression/cbmc-incr/sum_array_true1/test.desc index a907bb6415d..3e307e571fe 100644 --- a/regression/cbmc-incr/sum_array_true1/test.desc +++ b/regression/cbmc-incr/sum_array_true1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR --unwind-max 6 --no-unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc-incr/unwind-not-forever1/test.desc b/regression/cbmc-incr/unwind-not-forever1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-incr/unwind-not-forever1/test.desc +++ b/regression/cbmc-incr/unwind-not-forever1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-incr/unwind-not-forever2/test.desc b/regression/cbmc-incr/unwind-not-forever2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-incr/unwind-not-forever2/test.desc +++ b/regression/cbmc-incr/unwind-not-forever2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-incr/unwinding-assertion1/test.desc b/regression/cbmc-incr/unwinding-assertion1/test.desc index 3ede5ed0f72..efb176e1ccc 100644 --- a/regression/cbmc-incr/unwinding-assertion1/test.desc +++ b/regression/cbmc-incr/unwinding-assertion1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 10 ^EXIT=10$ diff --git a/regression/cbmc-incr/verisec_OpenSER__cases1_stripFullBoth_arr_false1/test.desc b/regression/cbmc-incr/verisec_OpenSER__cases1_stripFullBoth_arr_false1/test.desc index feb208278d1..fe5e0b6d27c 100644 --- a/regression/cbmc-incr/verisec_OpenSER__cases1_stripFullBoth_arr_false1/test.desc +++ b/regression/cbmc-incr/verisec_OpenSER__cases1_stripFullBoth_arr_false1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR --unwind-max 6 ^EXIT=10$ diff --git a/regression/cbmc-with-incr/ASHR1/test.desc b/regression/cbmc-with-incr/ASHR1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/ASHR1/test.desc +++ b/regression/cbmc-with-incr/ASHR1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Address_of1/test.desc b/regression/cbmc-with-incr/Address_of1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Address_of1/test.desc +++ b/regression/cbmc-with-incr/Address_of1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Address_of2/test.desc b/regression/cbmc-with-incr/Address_of2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Address_of2/test.desc +++ b/regression/cbmc-with-incr/Address_of2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Anonymous_Struct1/test.desc b/regression/cbmc-with-incr/Anonymous_Struct1/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Anonymous_Struct1/test.desc +++ b/regression/cbmc-with-incr/Anonymous_Struct1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Anonymous_Struct2/test.desc b/regression/cbmc-with-incr/Anonymous_Struct2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Anonymous_Struct2/test.desc +++ b/regression/cbmc-with-incr/Anonymous_Struct2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Anonymous_Struct3/test.desc b/regression/cbmc-with-incr/Anonymous_Struct3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Anonymous_Struct3/test.desc +++ b/regression/cbmc-with-incr/Anonymous_Struct3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Array_Initialization1/test.desc b/regression/cbmc-with-incr/Array_Initialization1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Array_Initialization1/test.desc +++ b/regression/cbmc-with-incr/Array_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Array_Initialization2/test.desc b/regression/cbmc-with-incr/Array_Initialization2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Array_Initialization2/test.desc +++ b/regression/cbmc-with-incr/Array_Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Array_Initialization3/test.desc b/regression/cbmc-with-incr/Array_Initialization3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Array_Initialization3/test.desc +++ b/regression/cbmc-with-incr/Array_Initialization3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Array_UF/test.desc b/regression/cbmc-with-incr/Array_UF/test.desc index 91cbd435ddd..d3d4443c8cb 100644 --- a/regression/cbmc-with-incr/Array_UF/test.desc +++ b/regression/cbmc-with-incr/Array_UF/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --arrays-uf-always ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Assumption1/test.desc b/regression/cbmc-with-incr/Assumption1/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Assumption1/test.desc +++ b/regression/cbmc-with-incr/Assumption1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/BV_Arithmetic1/test.desc b/regression/cbmc-with-incr/BV_Arithmetic1/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic1/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/BV_Arithmetic2/test.desc b/regression/cbmc-with-incr/BV_Arithmetic2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic2/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/BV_Arithmetic3/test.desc b/regression/cbmc-with-incr/BV_Arithmetic3/test.desc index d2a7e3e7574..e6ca0ec0299 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic3/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/BV_Arithmetic4/test.desc b/regression/cbmc-with-incr/BV_Arithmetic4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic4/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/BV_Arithmetic5/test.desc b/regression/cbmc-with-incr/BV_Arithmetic5/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic5/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/BV_Arithmetic6/test.desc b/regression/cbmc-with-incr/BV_Arithmetic6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic6/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Bitfields1/test.desc b/regression/cbmc-with-incr/Bitfields1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Bitfields1/test.desc +++ b/regression/cbmc-with-incr/Bitfields1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Bitfields2/test.desc b/regression/cbmc-with-incr/Bitfields2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Bitfields2/test.desc +++ b/regression/cbmc-with-incr/Bitfields2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Bool1/test.desc b/regression/cbmc-with-incr/Bool1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Bool1/test.desc +++ b/regression/cbmc-with-incr/Bool1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Bool2/test.desc b/regression/cbmc-with-incr/Bool2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Bool2/test.desc +++ b/regression/cbmc-with-incr/Bool2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Bool3/test.desc b/regression/cbmc-with-incr/Bool3/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/Bool3/test.desc +++ b/regression/cbmc-with-incr/Bool3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Bool4/test.desc b/regression/cbmc-with-incr/Bool4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Bool4/test.desc +++ b/regression/cbmc-with-incr/Bool4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Boolean_Guards1/test.desc b/regression/cbmc-with-incr/Boolean_Guards1/test.desc index da239c1965b..6550ede8bf0 100644 --- a/regression/cbmc-with-incr/Boolean_Guards1/test.desc +++ b/regression/cbmc-with-incr/Boolean_Guards1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --bounds-check --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/CMakeLists.txt b/regression/cbmc-with-incr/CMakeLists.txt new file mode 100644 index 00000000000..da7f7e70da7 --- /dev/null +++ b/regression/cbmc-with-incr/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$ --incremental" +) diff --git a/regression/cbmc-with-incr/Computed-Goto1/test.desc b/regression/cbmc-with-incr/Computed-Goto1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Computed-Goto1/test.desc +++ b/regression/cbmc-with-incr/Computed-Goto1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Division1/test.desc b/regression/cbmc-with-incr/Division1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Division1/test.desc +++ b/regression/cbmc-with-incr/Division1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Division2/test.desc b/regression/cbmc-with-incr/Division2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Division2/test.desc +++ b/regression/cbmc-with-incr/Division2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Double-to-float-no-simp1-fix1/test.desc b/regression/cbmc-with-incr/Double-to-float-no-simp1-fix1/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Double-to-float-no-simp1-fix1/test.desc +++ b/regression/cbmc-with-incr/Double-to-float-no-simp1-fix1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Double-to-float-no-simp1-fix2/test.desc b/regression/cbmc-with-incr/Double-to-float-no-simp1-fix2/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Double-to-float-no-simp1-fix2/test.desc +++ b/regression/cbmc-with-incr/Double-to-float-no-simp1-fix2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Double-to-float-no-simp1/test.desc b/regression/cbmc-with-incr/Double-to-float-no-simp1/test.desc index 26cf28c608c..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Double-to-float-no-simp1/test.desc +++ b/regression/cbmc-with-incr/Double-to-float-no-simp1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Double-to-float-with-simp1/test.desc b/regression/cbmc-with-incr/Double-to-float-with-simp1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Double-to-float-with-simp1/test.desc +++ b/regression/cbmc-with-incr/Double-to-float-with-simp1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Ellipsis1/test.desc b/regression/cbmc-with-incr/Ellipsis1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Ellipsis1/test.desc +++ b/regression/cbmc-with-incr/Ellipsis1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Ellipsis2/test.desc b/regression/cbmc-with-incr/Ellipsis2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Ellipsis2/test.desc +++ b/regression/cbmc-with-incr/Ellipsis2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness1/test.desc b/regression/cbmc-with-incr/Endianness1/test.desc index 217eac96e2f..ba4b3088aad 100644 --- a/regression/cbmc-with-incr/Endianness1/test.desc +++ b/regression/cbmc-with-incr/Endianness1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness2/test.desc b/regression/cbmc-with-incr/Endianness2/test.desc index 4f2eebc5e15..7a9dc127d75 100644 --- a/regression/cbmc-with-incr/Endianness2/test.desc +++ b/regression/cbmc-with-incr/Endianness2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness3/test.desc b/regression/cbmc-with-incr/Endianness3/test.desc index 217eac96e2f..ba4b3088aad 100644 --- a/regression/cbmc-with-incr/Endianness3/test.desc +++ b/regression/cbmc-with-incr/Endianness3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness4/test.desc b/regression/cbmc-with-incr/Endianness4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Endianness4/test.desc +++ b/regression/cbmc-with-incr/Endianness4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness5/test.desc b/regression/cbmc-with-incr/Endianness5/test.desc index 4e90da351ba..78c5c527dda 100644 --- a/regression/cbmc-with-incr/Endianness5/test.desc +++ b/regression/cbmc-with-incr/Endianness5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --little-endian --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness6/test.desc b/regression/cbmc-with-incr/Endianness6/test.desc index 81ceb4c6dc0..97280db41b7 100644 --- a/regression/cbmc-with-incr/Endianness6/test.desc +++ b/regression/cbmc-with-incr/Endianness6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness7/test.desc b/regression/cbmc-with-incr/Endianness7/test.desc index 54056d719c9..5c1f29271aa 100644 --- a/regression/cbmc-with-incr/Endianness7/test.desc +++ b/regression/cbmc-with-incr/Endianness7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --big-endian --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness8/test.desc b/regression/cbmc-with-incr/Endianness8/test.desc index 81ceb4c6dc0..97280db41b7 100644 --- a/regression/cbmc-with-incr/Endianness8/test.desc +++ b/regression/cbmc-with-incr/Endianness8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Endianness9/test.desc b/regression/cbmc-with-incr/Endianness9/test.desc index 76e90889ee9..97280db41b7 100644 --- a/regression/cbmc-with-incr/Endianness9/test.desc +++ b/regression/cbmc-with-incr/Endianness9/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Error_Label1/test.desc b/regression/cbmc-with-incr/Error_Label1/test.desc index e14ade773e5..954d11d1147 100644 --- a/regression/cbmc-with-incr/Error_Label1/test.desc +++ b/regression/cbmc-with-incr/Error_Label1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Error_Label2/test.desc b/regression/cbmc-with-incr/Error_Label2/test.desc index 3631d5c8930..9392434c203 100644 --- a/regression/cbmc-with-incr/Error_Label2/test.desc +++ b/regression/cbmc-with-incr/Error_Label2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR --no-assertions ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Error_Label3/test.desc b/regression/cbmc-with-incr/Error_Label3/test.desc index 450e47883c7..f8278beb10b 100644 --- a/regression/cbmc-with-incr/Error_Label3/test.desc +++ b/regression/cbmc-with-incr/Error_Label3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --error-label ERROR1 --error-label ERROR2 ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Eval_Order1/test.desc b/regression/cbmc-with-incr/Eval_Order1/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Eval_Order1/test.desc +++ b/regression/cbmc-with-incr/Eval_Order1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Exceptions1/test.desc b/regression/cbmc-with-incr/Exceptions1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Exceptions1/test.desc +++ b/regression/cbmc-with-incr/Exceptions1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Failing_Assert1/test.desc b/regression/cbmc-with-incr/Failing_Assert1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/Failing_Assert1/test.desc +++ b/regression/cbmc-with-incr/Failing_Assert1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Fixedbv1/test.desc b/regression/cbmc-with-incr/Fixedbv1/test.desc index 991a8916c67..53abd750f68 100644 --- a/regression/cbmc-with-incr/Fixedbv1/test.desc +++ b/regression/cbmc-with-incr/Fixedbv1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Fixedbv2/test.desc b/regression/cbmc-with-incr/Fixedbv2/test.desc index 991a8916c67..53abd750f68 100644 --- a/regression/cbmc-with-incr/Fixedbv2/test.desc +++ b/regression/cbmc-with-incr/Fixedbv2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Fixedbv3/test.desc b/regression/cbmc-with-incr/Fixedbv3/test.desc index 991a8916c67..53abd750f68 100644 --- a/regression/cbmc-with-incr/Fixedbv3/test.desc +++ b/regression/cbmc-with-incr/Fixedbv3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Fixedbv4/test.desc b/regression/cbmc-with-incr/Fixedbv4/test.desc index a43bbd7df65..dcd58b05b14 100644 --- a/regression/cbmc-with-incr/Fixedbv4/test.desc +++ b/regression/cbmc-with-incr/Fixedbv4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Fixedbv5/test.desc b/regression/cbmc-with-incr/Fixedbv5/test.desc index 991a8916c67..53abd750f68 100644 --- a/regression/cbmc-with-incr/Fixedbv5/test.desc +++ b/regression/cbmc-with-incr/Fixedbv5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Fixedbv6/test.desc b/regression/cbmc-with-incr/Fixedbv6/test.desc index 991a8916c67..53abd750f68 100644 --- a/regression/cbmc-with-incr/Fixedbv6/test.desc +++ b/regression/cbmc-with-incr/Fixedbv6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Fixedbv7/test.desc b/regression/cbmc-with-incr/Fixedbv7/test.desc index 5b018497756..660c72500af 100644 --- a/regression/cbmc-with-incr/Fixedbv7/test.desc +++ b/regression/cbmc-with-incr/Fixedbv7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --fixedbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-Rounding1/test.desc b/regression/cbmc-with-incr/Float-Rounding1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float-Rounding1/test.desc +++ b/regression/cbmc-with-incr/Float-Rounding1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-Rounding2/test.desc b/regression/cbmc-with-incr/Float-Rounding2/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float-Rounding2/test.desc +++ b/regression/cbmc-with-incr/Float-Rounding2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-data-dependent-rounding/test.desc b/regression/cbmc-with-incr/Float-data-dependent-rounding/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Float-data-dependent-rounding/test.desc +++ b/regression/cbmc-with-incr/Float-data-dependent-rounding/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-div1/test.desc b/regression/cbmc-with-incr/Float-div1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float-div1/test.desc +++ b/regression/cbmc-with-incr/Float-div1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-flags-no-simp1/test.desc b/regression/cbmc-with-incr/Float-flags-no-simp1/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-flags-no-simp1/test.desc +++ b/regression/cbmc-with-incr/Float-flags-no-simp1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-flags-simp1/test.desc b/regression/cbmc-with-incr/Float-flags-simp1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float-flags-simp1/test.desc +++ b/regression/cbmc-with-incr/Float-flags-simp1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp1/test.desc b/regression/cbmc-with-incr/Float-no-simp1/test.desc index 376d43d5dfa..b7c95d95569 100644 --- a/regression/cbmc-with-incr/Float-no-simp1/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp2/test.desc b/regression/cbmc-with-incr/Float-no-simp2/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp2/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp3/test.desc b/regression/cbmc-with-incr/Float-no-simp3/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp3/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp4/test.desc b/regression/cbmc-with-incr/Float-no-simp4/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp4/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp5/test.desc b/regression/cbmc-with-incr/Float-no-simp5/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp5/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp6/test.desc b/regression/cbmc-with-incr/Float-no-simp6/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp6/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp7/test.desc b/regression/cbmc-with-incr/Float-no-simp7/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp7/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp8/test.desc b/regression/cbmc-with-incr/Float-no-simp8/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp8/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-no-simp9/test.desc b/regression/cbmc-with-incr/Float-no-simp9/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-no-simp9/test.desc +++ b/regression/cbmc-with-incr/Float-no-simp9/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-overflow1/test.desc b/regression/cbmc-with-incr/Float-overflow1/test.desc index a1de3d41cf0..34ceb2ef1d1 100644 --- a/regression/cbmc-with-incr/Float-overflow1/test.desc +++ b/regression/cbmc-with-incr/Float-overflow1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --float-overflow-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-overflow2/test.desc b/regression/cbmc-with-incr/Float-overflow2/test.desc index f7cd5fc8bf3..fe62098e887 100644 --- a/regression/cbmc-with-incr/Float-overflow2/test.desc +++ b/regression/cbmc-with-incr/Float-overflow2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --float-overflow-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Float-to-double1/test.desc b/regression/cbmc-with-incr/Float-to-double1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float-to-double1/test.desc +++ b/regression/cbmc-with-incr/Float-to-double1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-to-double2/test.desc b/regression/cbmc-with-incr/Float-to-double2/test.desc index 4d2a93e6e26..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-to-double2/test.desc +++ b/regression/cbmc-with-incr/Float-to-double2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float-zero-sum1/test.desc b/regression/cbmc-with-incr/Float-zero-sum1/test.desc index 26cf28c608c..dc9e039b99a 100644 --- a/regression/cbmc-with-incr/Float-zero-sum1/test.desc +++ b/regression/cbmc-with-incr/Float-zero-sum1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --floatbv --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float1/test.desc b/regression/cbmc-with-incr/Float1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float1/test.desc +++ b/regression/cbmc-with-incr/Float1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float11/test.desc b/regression/cbmc-with-incr/Float11/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float11/test.desc +++ b/regression/cbmc-with-incr/Float11/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float12/test.desc b/regression/cbmc-with-incr/Float12/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Float12/test.desc +++ b/regression/cbmc-with-incr/Float12/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float13/test.desc b/regression/cbmc-with-incr/Float13/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Float13/test.desc +++ b/regression/cbmc-with-incr/Float13/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float14/test.desc b/regression/cbmc-with-incr/Float14/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Float14/test.desc +++ b/regression/cbmc-with-incr/Float14/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float18/test.desc b/regression/cbmc-with-incr/Float18/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float18/test.desc +++ b/regression/cbmc-with-incr/Float18/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float19/test.desc b/regression/cbmc-with-incr/Float19/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float19/test.desc +++ b/regression/cbmc-with-incr/Float19/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float2/test.desc b/regression/cbmc-with-incr/Float2/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float2/test.desc +++ b/regression/cbmc-with-incr/Float2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float20/test.desc b/regression/cbmc-with-incr/Float20/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float20/test.desc +++ b/regression/cbmc-with-incr/Float20/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float21/test.desc b/regression/cbmc-with-incr/Float21/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float21/test.desc +++ b/regression/cbmc-with-incr/Float21/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float22/test.desc b/regression/cbmc-with-incr/Float22/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float22/test.desc +++ b/regression/cbmc-with-incr/Float22/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float3/test.desc b/regression/cbmc-with-incr/Float3/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float3/test.desc +++ b/regression/cbmc-with-incr/Float3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float4/test.desc b/regression/cbmc-with-incr/Float4/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float4/test.desc +++ b/regression/cbmc-with-incr/Float4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float5/test.desc b/regression/cbmc-with-incr/Float5/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float5/test.desc +++ b/regression/cbmc-with-incr/Float5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float6/test.desc b/regression/cbmc-with-incr/Float6/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float6/test.desc +++ b/regression/cbmc-with-incr/Float6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float7/test.desc b/regression/cbmc-with-incr/Float7/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Float7/test.desc +++ b/regression/cbmc-with-incr/Float7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float8/test.desc b/regression/cbmc-with-incr/Float8/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Float8/test.desc +++ b/regression/cbmc-with-incr/Float8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float_lib1/test.desc b/regression/cbmc-with-incr/Float_lib1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float_lib1/test.desc +++ b/regression/cbmc-with-incr/Float_lib1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Float_lib2/test.desc b/regression/cbmc-with-incr/Float_lib2/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/Float_lib2/test.desc +++ b/regression/cbmc-with-incr/Float_lib2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Free1/test.desc b/regression/cbmc-with-incr/Free1/test.desc index 02f1049518a..90d1fb1d263 100644 --- a/regression/cbmc-with-incr/Free1/test.desc +++ b/regression/cbmc-with-incr/Free1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Free2/test.desc b/regression/cbmc-with-incr/Free2/test.desc index 02f1049518a..90d1fb1d263 100644 --- a/regression/cbmc-with-incr/Free2/test.desc +++ b/regression/cbmc-with-incr/Free2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Free3/test.desc b/regression/cbmc-with-incr/Free3/test.desc index fd1b888b81d..7cb31bd31f9 100644 --- a/regression/cbmc-with-incr/Free3/test.desc +++ b/regression/cbmc-with-incr/Free3/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE main.c --pointer-check +^EXIT=10$ ^SIGNAL=0$ -^Counterexample:$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Free4/test.desc b/regression/cbmc-with-incr/Free4/test.desc index fd1b888b81d..7cb31bd31f9 100644 --- a/regression/cbmc-with-incr/Free4/test.desc +++ b/regression/cbmc-with-incr/Free4/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE main.c --pointer-check +^EXIT=10$ ^SIGNAL=0$ -^Counterexample:$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Function-KnR1/test.desc b/regression/cbmc-with-incr/Function-KnR1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function-KnR1/test.desc +++ b/regression/cbmc-with-incr/Function-KnR1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function1/test.desc b/regression/cbmc-with-incr/Function1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function1/test.desc +++ b/regression/cbmc-with-incr/Function1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function10/test.desc b/regression/cbmc-with-incr/Function10/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function10/test.desc +++ b/regression/cbmc-with-incr/Function10/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function11/test.desc b/regression/cbmc-with-incr/Function11/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function11/test.desc +++ b/regression/cbmc-with-incr/Function11/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function12/test.desc b/regression/cbmc-with-incr/Function12/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function12/test.desc +++ b/regression/cbmc-with-incr/Function12/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function13/test.desc b/regression/cbmc-with-incr/Function13/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function13/test.desc +++ b/regression/cbmc-with-incr/Function13/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function2/test.desc b/regression/cbmc-with-incr/Function2/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Function2/test.desc +++ b/regression/cbmc-with-incr/Function2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Function3/test.desc b/regression/cbmc-with-incr/Function3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function3/test.desc +++ b/regression/cbmc-with-incr/Function3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function4/test.desc b/regression/cbmc-with-incr/Function4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function4/test.desc +++ b/regression/cbmc-with-incr/Function4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function5/test.desc b/regression/cbmc-with-incr/Function5/test.desc index 50371f73fff..9a3c0c12d69 100644 --- a/regression/cbmc-with-incr/Function5/test.desc +++ b/regression/cbmc-with-incr/Function5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^SIGNAL=0$ diff --git a/regression/cbmc-with-incr/Function6/test.desc b/regression/cbmc-with-incr/Function6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function6/test.desc +++ b/regression/cbmc-with-incr/Function6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function7/test.desc b/regression/cbmc-with-incr/Function7/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function7/test.desc +++ b/regression/cbmc-with-incr/Function7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function8/test.desc b/regression/cbmc-with-incr/Function8/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Function8/test.desc +++ b/regression/cbmc-with-incr/Function8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Function9/test.desc b/regression/cbmc-with-incr/Function9/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Function9/test.desc +++ b/regression/cbmc-with-incr/Function9/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Function_Eval_Order2/test.desc b/regression/cbmc-with-incr/Function_Eval_Order2/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Function_Eval_Order2/test.desc +++ b/regression/cbmc-with-incr/Function_Eval_Order2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Function_Parameters1/test.desc b/regression/cbmc-with-incr/Function_Parameters1/test.desc index fc2b1874059..f98f52c58e3 100644 --- a/regression/cbmc-with-incr/Function_Parameters1/test.desc +++ b/regression/cbmc-with-incr/Function_Parameters1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer1/test.desc b/regression/cbmc-with-incr/Function_Pointer1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer1/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer10/test.desc b/regression/cbmc-with-incr/Function_Pointer10/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer10/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer10/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer11/test.desc b/regression/cbmc-with-incr/Function_Pointer11/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer11/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer11/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer12/test.desc b/regression/cbmc-with-incr/Function_Pointer12/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer12/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer12/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer13/test.desc b/regression/cbmc-with-incr/Function_Pointer13/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer13/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer13/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer14/test.desc b/regression/cbmc-with-incr/Function_Pointer14/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Function_Pointer14/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer14/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer15/test.desc b/regression/cbmc-with-incr/Function_Pointer15/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/Function_Pointer15/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer15/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Function_Pointer16/test.desc b/regression/cbmc-with-incr/Function_Pointer16/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Function_Pointer16/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer16/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer17/test.desc b/regression/cbmc-with-incr/Function_Pointer17/test.desc index b5f3e5b3c93..58806af6ac6 100644 --- a/regression/cbmc-with-incr/Function_Pointer17/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer17/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 1 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer2/test.desc b/regression/cbmc-with-incr/Function_Pointer2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer2/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer3/test.desc b/regression/cbmc-with-incr/Function_Pointer3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer3/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer4/test.desc b/regression/cbmc-with-incr/Function_Pointer4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer4/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer5/test.desc b/regression/cbmc-with-incr/Function_Pointer5/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer5/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer6/test.desc b/regression/cbmc-with-incr/Function_Pointer6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer6/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer7/test.desc b/regression/cbmc-with-incr/Function_Pointer7/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Function_Pointer7/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Function_Pointer8/test.desc b/regression/cbmc-with-incr/Function_Pointer8/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Function_Pointer8/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Function_Pointer9/test.desc b/regression/cbmc-with-incr/Function_Pointer9/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Function_Pointer9/test.desc +++ b/regression/cbmc-with-incr/Function_Pointer9/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Global_Initialization1/test.desc b/regression/cbmc-with-incr/Global_Initialization1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Global_Initialization1/test.desc +++ b/regression/cbmc-with-incr/Global_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Global_Initialization2/test.desc b/regression/cbmc-with-incr/Global_Initialization2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Global_Initialization2/test.desc +++ b/regression/cbmc-with-incr/Global_Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Initialization1/test.desc b/regression/cbmc-with-incr/Initialization1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Initialization1/test.desc +++ b/regression/cbmc-with-incr/Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Initialization2/test.desc b/regression/cbmc-with-incr/Initialization2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Initialization2/test.desc +++ b/regression/cbmc-with-incr/Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Initialization3/test.desc b/regression/cbmc-with-incr/Initialization3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Initialization3/test.desc +++ b/regression/cbmc-with-incr/Initialization3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Initialization5/test.desc b/regression/cbmc-with-incr/Initialization5/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/Initialization5/test.desc +++ b/regression/cbmc-with-incr/Initialization5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Initialization6/test.desc b/regression/cbmc-with-incr/Initialization6/test.desc index fb5fd7bb84f..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Initialization6/test.desc +++ b/regression/cbmc-with-incr/Initialization6/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Initialization7/test.desc b/regression/cbmc-with-incr/Initialization7/test.desc index fb5fd7bb84f..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Initialization7/test.desc +++ b/regression/cbmc-with-incr/Initialization7/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Linking1/test.desc b/regression/cbmc-with-incr/Linking1/test.desc index af20f90c655..b302e1734c3 100644 --- a/regression/cbmc-with-incr/Linking1/test.desc +++ b/regression/cbmc-with-incr/Linking1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c module.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Linking2/test.desc b/regression/cbmc-with-incr/Linking2/test.desc index af20f90c655..b302e1734c3 100644 --- a/regression/cbmc-with-incr/Linking2/test.desc +++ b/regression/cbmc-with-incr/Linking2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c module.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Linking3/test.desc b/regression/cbmc-with-incr/Linking3/test.desc index bb271770fef..eac92128f48 100644 --- a/regression/cbmc-with-incr/Linking3/test.desc +++ b/regression/cbmc-with-incr/Linking3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main1.c main2.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Linking4/test.desc b/regression/cbmc-with-incr/Linking4/test.desc index d88e6744dbd..e55c8af1212 100644 --- a/regression/cbmc-with-incr/Linking4/test.desc +++ b/regression/cbmc-with-incr/Linking4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE link1.c link2.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Local_out_of_scope1/test.desc b/regression/cbmc-with-incr/Local_out_of_scope1/test.desc index 950f6791fef..7cb31bd31f9 100644 --- a/regression/cbmc-with-incr/Local_out_of_scope1/test.desc +++ b/regression/cbmc-with-incr/Local_out_of_scope1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Malloc13/test.desc b/regression/cbmc-with-incr/Malloc13/test.desc index f3145b289ad..24c71045fd8 100644 --- a/regression/cbmc-with-incr/Malloc13/test.desc +++ b/regression/cbmc-with-incr/Malloc13/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc14/test.desc b/regression/cbmc-with-incr/Malloc14/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/Malloc14/test.desc +++ b/regression/cbmc-with-incr/Malloc14/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc15/test.desc b/regression/cbmc-with-incr/Malloc15/test.desc index f046159d042..b2b85f25827 100644 --- a/regression/cbmc-with-incr/Malloc15/test.desc +++ b/regression/cbmc-with-incr/Malloc15/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --32 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc16/test.desc b/regression/cbmc-with-incr/Malloc16/test.desc index f046159d042..b2b85f25827 100644 --- a/regression/cbmc-with-incr/Malloc16/test.desc +++ b/regression/cbmc-with-incr/Malloc16/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --32 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc17/test.desc b/regression/cbmc-with-incr/Malloc17/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/Malloc17/test.desc +++ b/regression/cbmc-with-incr/Malloc17/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc18/test.desc b/regression/cbmc-with-incr/Malloc18/test.desc index a27d6e3414c..fb6666914d4 100644 --- a/regression/cbmc-with-incr/Malloc18/test.desc +++ b/regression/cbmc-with-incr/Malloc18/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc19/test.desc b/regression/cbmc-with-incr/Malloc19/test.desc index a27d6e3414c..fb6666914d4 100644 --- a/regression/cbmc-with-incr/Malloc19/test.desc +++ b/regression/cbmc-with-incr/Malloc19/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Malloc20/test.desc b/regression/cbmc-with-incr/Malloc20/test.desc index a27d6e3414c..fb6666914d4 100644 --- a/regression/cbmc-with-incr/Malloc20/test.desc +++ b/regression/cbmc-with-incr/Malloc20/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Memmove1/test.desc b/regression/cbmc-with-incr/Memmove1/test.desc index c0092d0ee56..76e601983c1 100644 --- a/regression/cbmc-with-incr/Memmove1/test.desc +++ b/regression/cbmc-with-incr/Memmove1/test.desc @@ -1,4 +1,4 @@ -THOROUGH +FUTURE main.c --unwind 17 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Memory_leak1/test.desc b/regression/cbmc-with-incr/Memory_leak1/test.desc index 91591a9814c..4a3deeb99a4 100644 --- a/regression/cbmc-with-incr/Memory_leak1/test.desc +++ b/regression/cbmc-with-incr/Memory_leak1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --memory-leak-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Memory_leak2/test.desc b/regression/cbmc-with-incr/Memory_leak2/test.desc index f90f7c4f8f1..9d475e80a99 100644 --- a/regression/cbmc-with-incr/Memory_leak2/test.desc +++ b/regression/cbmc-with-incr/Memory_leak2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --memory-leak-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Mod1/test.desc b/regression/cbmc-with-incr/Mod1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/Mod1/test.desc +++ b/regression/cbmc-with-incr/Mod1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Mod2/test.desc b/regression/cbmc-with-incr/Mod2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Mod2/test.desc +++ b/regression/cbmc-with-incr/Mod2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array1/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array1/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array2/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array2/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array3/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array3/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array4/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array4/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array5/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array5/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array5/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc index c171dd49a18..083aef95321 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unwind-max 3 --no-unwinding-assertions --all-properties ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Negation1/test.desc b/regression/cbmc-with-incr/Negation1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Negation1/test.desc +++ b/regression/cbmc-with-incr/Negation1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Negation2/test.desc b/regression/cbmc-with-incr/Negation2/test.desc index cbd90510599..415020cf03f 100644 --- a/regression/cbmc-with-incr/Negation2/test.desc +++ b/regression/cbmc-with-incr/Negation2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-propagation ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Overflow_Addition1/test.desc b/regression/cbmc-with-incr/Overflow_Addition1/test.desc index 5dbaca0c795..846e5400516 100644 --- a/regression/cbmc-with-incr/Overflow_Addition1/test.desc +++ b/regression/cbmc-with-incr/Overflow_Addition1/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE main.c --signed-overflow-check +^EXIT=10$ ^SIGNAL=0$ -^Counterexample:$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Overflow_Multiplication1/test.desc b/regression/cbmc-with-incr/Overflow_Multiplication1/test.desc index a83213498f1..161b62e81d1 100644 --- a/regression/cbmc-with-incr/Overflow_Multiplication1/test.desc +++ b/regression/cbmc-with-incr/Overflow_Multiplication1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE falsealarm.c --signed-overflow-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic1/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic1/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic1/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic10/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic10/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic10/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic10/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic11/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic11/test.desc index f5e039ba3ed..d6d68d98e98 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic11/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic11/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --little-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic12/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic12/test.desc index 3de54602985..38d939ef120 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic12/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic12/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --32 --little-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic13/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic13/test.desc index 52168c7eba4..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic13/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic13/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic2/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic2/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic2/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic3/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic3/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic3/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic4/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic4/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic4/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc index 73810cf4375..d1dc65c4c82 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE main.c --pointer-check --bounds-check --function f +^EXIT=10$ ^SIGNAL=0$ -^Counterexample:$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic6/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic6/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic6/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic7/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic7/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic7/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc index 0f0f5660f42..d3f7d2d7cdd 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE main.c --pointer-check --bounds-check +^EXIT=10$ ^SIGNAL=0$ -^Counterexample:$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic9/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic9/test.desc index 39c491ba8bb..873bd8d918c 100644 --- a/regression/cbmc-with-incr/Pointer_Arithmetic9/test.desc +++ b/regression/cbmc-with-incr/Pointer_Arithmetic9/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_Assume1/test.desc b/regression/cbmc-with-incr/Pointer_Assume1/test.desc index a27d6e3414c..fb6666914d4 100644 --- a/regression/cbmc-with-incr/Pointer_Assume1/test.desc +++ b/regression/cbmc-with-incr/Pointer_Assume1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_array1/test.desc b/regression/cbmc-with-incr/Pointer_array1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Pointer_array1/test.desc +++ b/regression/cbmc-with-incr/Pointer_array1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_array2/test.desc b/regression/cbmc-with-incr/Pointer_array2/test.desc index 52168c7eba4..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Pointer_array2/test.desc +++ b/regression/cbmc-with-incr/Pointer_array2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract1/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract1/test.desc index 12fc8ce06e1..8681f1ad0e1 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract1/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc index ad9c2b40bd5..2b370199c4c 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --all-properties --little-endian ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract3/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract3/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract4/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract4/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc index 47c1a75edbe..a3e0bed53f3 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --all-properties --bounds-check --32 ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract6/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract6/test.desc index 466da18b2b5..f98f52c58e3 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract6/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract7/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract7/test.desc index 81ceb4c6dc0..97280db41b7 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract7/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc index a8688dd7116..58fb9a48fbe 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --all-properties --bounds-check --32 --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Pointer_difference1/test.desc b/regression/cbmc-with-incr/Pointer_difference1/test.desc index 466da18b2b5..f98f52c58e3 100644 --- a/regression/cbmc-with-incr/Pointer_difference1/test.desc +++ b/regression/cbmc-with-incr/Pointer_difference1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Promotion1/test.desc b/regression/cbmc-with-incr/Promotion1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Promotion1/test.desc +++ b/regression/cbmc-with-incr/Promotion1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Promotion2/test.desc b/regression/cbmc-with-incr/Promotion2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Promotion2/test.desc +++ b/regression/cbmc-with-incr/Promotion2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Quantifiers1/test.desc b/regression/cbmc-with-incr/Quantifiers1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Quantifiers1/test.desc +++ b/regression/cbmc-with-incr/Quantifiers1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Recursion1/test.desc b/regression/cbmc-with-incr/Recursion1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Recursion1/test.desc +++ b/regression/cbmc-with-incr/Recursion1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Recursion2/test.desc b/regression/cbmc-with-incr/Recursion2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Recursion2/test.desc +++ b/regression/cbmc-with-incr/Recursion2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Recursion3/test.desc b/regression/cbmc-with-incr/Recursion3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Recursion3/test.desc +++ b/regression/cbmc-with-incr/Recursion3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Recursion4/test.desc b/regression/cbmc-with-incr/Recursion4/test.desc index cbd90510599..415020cf03f 100644 --- a/regression/cbmc-with-incr/Recursion4/test.desc +++ b/regression/cbmc-with-incr/Recursion4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-propagation ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Recursion5/test.desc b/regression/cbmc-with-incr/Recursion5/test.desc index 8e070292fba..1c9b5265bd0 100644 --- a/regression/cbmc-with-incr/Recursion5/test.desc +++ b/regression/cbmc-with-incr/Recursion5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --earliest-loop-exit ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Recursion6/test.desc b/regression/cbmc-with-incr/Recursion6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Recursion6/test.desc +++ b/regression/cbmc-with-incr/Recursion6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Sideeffects1/test.desc b/regression/cbmc-with-incr/Sideeffects1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Sideeffects1/test.desc +++ b/regression/cbmc-with-incr/Sideeffects1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Sideeffects2/test.desc b/regression/cbmc-with-incr/Sideeffects2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Sideeffects2/test.desc +++ b/regression/cbmc-with-incr/Sideeffects2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Sideeffects3/test.desc b/regression/cbmc-with-incr/Sideeffects3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Sideeffects3/test.desc +++ b/regression/cbmc-with-incr/Sideeffects3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Sideeffects4/test.desc b/regression/cbmc-with-incr/Sideeffects4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Sideeffects4/test.desc +++ b/regression/cbmc-with-incr/Sideeffects4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Sideeffects5/test.desc b/regression/cbmc-with-incr/Sideeffects5/test.desc index e69488b2e66..2e26534178b 100644 --- a/regression/cbmc-with-incr/Sideeffects5/test.desc +++ b/regression/cbmc-with-incr/Sideeffects5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --div-by-zero-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Sideeffects6/test.desc b/regression/cbmc-with-incr/Sideeffects6/test.desc index e69488b2e66..2e26534178b 100644 --- a/regression/cbmc-with-incr/Sideeffects6/test.desc +++ b/regression/cbmc-with-incr/Sideeffects6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --div-by-zero-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Static2/test.desc b/regression/cbmc-with-incr/Static2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Static2/test.desc +++ b/regression/cbmc-with-incr/Static2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Static_Functions1/test.desc b/regression/cbmc-with-incr/Static_Functions1/test.desc index 8a09111c3b1..de55fd28989 100644 --- a/regression/cbmc-with-incr/Static_Functions1/test.desc +++ b/regression/cbmc-with-incr/Static_Functions1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE file1.c file2.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/String1/test.desc b/regression/cbmc-with-incr/String1/test.desc index 96c9b4bcd7b..b1749fa8cd6 100644 --- a/regression/cbmc-with-incr/String1/test.desc +++ b/regression/cbmc-with-incr/String1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/String2/test.desc b/regression/cbmc-with-incr/String2/test.desc index 75352ab9ea5..f632dbb059b 100644 --- a/regression/cbmc-with-incr/String2/test.desc +++ b/regression/cbmc-with-incr/String2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/String3/test.desc b/regression/cbmc-with-incr/String3/test.desc index e19d0a66341..f632dbb059b 100644 --- a/regression/cbmc-with-incr/String3/test.desc +++ b/regression/cbmc-with-incr/String3/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --pointer-check --bounds-check ^EXIT=10$ diff --git a/regression/cbmc-with-incr/String4/test.desc b/regression/cbmc-with-incr/String4/test.desc index 96c9b4bcd7b..b1749fa8cd6 100644 --- a/regression/cbmc-with-incr/String4/test.desc +++ b/regression/cbmc-with-incr/String4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/String5/test.desc b/regression/cbmc-with-incr/String5/test.desc index 96c9b4bcd7b..b1749fa8cd6 100644 --- a/regression/cbmc-with-incr/String5/test.desc +++ b/regression/cbmc-with-incr/String5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/String6/test.desc b/regression/cbmc-with-incr/String6/test.desc index 96c9b4bcd7b..b1749fa8cd6 100644 --- a/regression/cbmc-with-incr/String6/test.desc +++ b/regression/cbmc-with-incr/String6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/String7/test.desc b/regression/cbmc-with-incr/String7/test.desc index 96c9b4bcd7b..b1749fa8cd6 100644 --- a/regression/cbmc-with-incr/String7/test.desc +++ b/regression/cbmc-with-incr/String7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/String_Literal1/test.desc b/regression/cbmc-with-incr/String_Literal1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/String_Literal1/test.desc +++ b/regression/cbmc-with-incr/String_Literal1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Bytewise1/test.desc b/regression/cbmc-with-incr/Struct_Bytewise1/test.desc index 03ad7634d7c..da870488cb7 100644 --- a/regression/cbmc-with-incr/Struct_Bytewise1/test.desc +++ b/regression/cbmc-with-incr/Struct_Bytewise1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE struct_bytewise.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Bytewise2/test.desc b/regression/cbmc-with-incr/Struct_Bytewise2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Bytewise2/test.desc +++ b/regression/cbmc-with-incr/Struct_Bytewise2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization1/test.desc b/regression/cbmc-with-incr/Struct_Initialization1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization1/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization10/test.desc b/regression/cbmc-with-incr/Struct_Initialization10/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization10/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization10/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization2/test.desc b/regression/cbmc-with-incr/Struct_Initialization2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization2/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization3/test.desc b/regression/cbmc-with-incr/Struct_Initialization3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization3/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization4/test.desc b/regression/cbmc-with-incr/Struct_Initialization4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization4/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization5/test.desc b/regression/cbmc-with-incr/Struct_Initialization5/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization5/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization6/test.desc b/regression/cbmc-with-incr/Struct_Initialization6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization6/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization7/test.desc b/regression/cbmc-with-incr/Struct_Initialization7/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization7/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Initialization9/test.desc b/regression/cbmc-with-incr/Struct_Initialization9/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Struct_Initialization9/test.desc +++ b/regression/cbmc-with-incr/Struct_Initialization9/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Struct_Padding1/test.desc b/regression/cbmc-with-incr/Struct_Padding1/test.desc index 0098f266ed3..7d82bcc8fbb 100644 --- a/regression/cbmc-with-incr/Struct_Padding1/test.desc +++ b/regression/cbmc-with-incr/Struct_Padding1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --32 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Typecast1/test.desc b/regression/cbmc-with-incr/Typecast1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Typecast1/test.desc +++ b/regression/cbmc-with-incr/Typecast1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Typecast2/test.desc b/regression/cbmc-with-incr/Typecast2/test.desc index 1af9f7644e7..2f9be87fcce 100644 --- a/regression/cbmc-with-incr/Typecast2/test.desc +++ b/regression/cbmc-with-incr/Typecast2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-propagation --64 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Undefined_Function1/test.desc b/regression/cbmc-with-incr/Undefined_Function1/test.desc index d29ea2fc36e..56d593a23d6 100644 --- a/regression/cbmc-with-incr/Undefined_Function1/test.desc +++ b/regression/cbmc-with-incr/Undefined_Function1/test.desc @@ -1,9 +1,9 @@ -CORE +FUTURE main.c +^EXIT=10$ ^SIGNAL=0$ ^\*\*\*\* WARNING: no body for function f$ -^Counterexample:$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Union_Initialization1/test.desc b/regression/cbmc-with-incr/Union_Initialization1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Union_Initialization1/test.desc +++ b/regression/cbmc-with-incr/Union_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Unwinding_Locality1/test.desc b/regression/cbmc-with-incr/Unwinding_Locality1/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/Unwinding_Locality1/test.desc +++ b/regression/cbmc-with-incr/Unwinding_Locality1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Visual_Studio_Types1/test.desc b/regression/cbmc-with-incr/Visual_Studio_Types1/test.desc index e59b02c324d..481c817218a 100644 --- a/regression/cbmc-with-incr/Visual_Studio_Types1/test.desc +++ b/regression/cbmc-with-incr/Visual_Studio_Types1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --i386-win32 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Visual_Studio_Types2/test.desc b/regression/cbmc-with-incr/Visual_Studio_Types2/test.desc index 7ce542782ab..7b07e0dc555 100644 --- a/regression/cbmc-with-incr/Visual_Studio_Types2/test.desc +++ b/regression/cbmc-with-incr/Visual_Studio_Types2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --winx64 ^EXIT=0$ diff --git a/regression/cbmc-with-incr/Volatile1/test.desc b/regression/cbmc-with-incr/Volatile1/test.desc index 6b765c70f48..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/Volatile1/test.desc +++ b/regression/cbmc-with-incr/Volatile1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/Zero_Initialization1/test.desc b/regression/cbmc-with-incr/Zero_Initialization1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/Zero_Initialization1/test.desc +++ b/regression/cbmc-with-incr/Zero_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/__func__1/test.desc b/regression/cbmc-with-incr/__func__1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/__func__1/test.desc +++ b/regression/cbmc-with-incr/__func__1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/abs1/test.desc b/regression/cbmc-with-incr/abs1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/abs1/test.desc +++ b/regression/cbmc-with-incr/abs1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/argv1/test.desc b/regression/cbmc-with-incr/argv1/test.desc index da239c1965b..6550ede8bf0 100644 --- a/regression/cbmc-with-incr/argv1/test.desc +++ b/regression/cbmc-with-incr/argv1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --bounds-check --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/atomic_section_seq1/test.desc b/regression/cbmc-with-incr/atomic_section_seq1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/atomic_section_seq1/test.desc +++ b/regression/cbmc-with-incr/atomic_section_seq1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/char1/test.desc b/regression/cbmc-with-incr/char1/test.desc index ec0541ac9fc..a269860affb 100644 --- a/regression/cbmc-with-incr/char1/test.desc +++ b/regression/cbmc-with-incr/char1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unsigned-char ^EXIT=0$ diff --git a/regression/cbmc-with-incr/character_handling1/test.desc b/regression/cbmc-with-incr/character_handling1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/character_handling1/test.desc +++ b/regression/cbmc-with-incr/character_handling1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/comma1/test.desc b/regression/cbmc-with-incr/comma1/test.desc index 12fc8ce06e1..8681f1ad0e1 100644 --- a/regression/cbmc-with-incr/comma1/test.desc +++ b/regression/cbmc-with-incr/comma1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/complex1/test.desc b/regression/cbmc-with-incr/complex1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/complex1/test.desc +++ b/regression/cbmc-with-incr/complex1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/compound_literal1/test.desc b/regression/cbmc-with-incr/compound_literal1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/compound_literal1/test.desc +++ b/regression/cbmc-with-incr/compound_literal1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/const_ptr1/test.desc b/regression/cbmc-with-incr/const_ptr1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/const_ptr1/test.desc +++ b/regression/cbmc-with-incr/const_ptr1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/enum1/test.desc b/regression/cbmc-with-incr/enum1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/enum1/test.desc +++ b/regression/cbmc-with-incr/enum1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/enum2/test.desc b/regression/cbmc-with-incr/enum2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/enum2/test.desc +++ b/regression/cbmc-with-incr/enum2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/enum3/test.desc b/regression/cbmc-with-incr/enum3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/enum3/test.desc +++ b/regression/cbmc-with-incr/enum3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/enum4/test.desc b/regression/cbmc-with-incr/enum4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/enum4/test.desc +++ b/regression/cbmc-with-incr/enum4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array1/test.desc b/regression/cbmc-with-incr/equality_through_array1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array1/test.desc +++ b/regression/cbmc-with-incr/equality_through_array1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array2/test.desc b/regression/cbmc-with-incr/equality_through_array2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array2/test.desc +++ b/regression/cbmc-with-incr/equality_through_array2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array3/test.desc b/regression/cbmc-with-incr/equality_through_array3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array3/test.desc +++ b/regression/cbmc-with-incr/equality_through_array3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array4/test.desc b/regression/cbmc-with-incr/equality_through_array4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array4/test.desc +++ b/regression/cbmc-with-incr/equality_through_array4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array5/test.desc b/regression/cbmc-with-incr/equality_through_array5/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array5/test.desc +++ b/regression/cbmc-with-incr/equality_through_array5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array6/test.desc b/regression/cbmc-with-incr/equality_through_array6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array6/test.desc +++ b/regression/cbmc-with-incr/equality_through_array6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array_of_struct1/test.desc b/regression/cbmc-with-incr/equality_through_array_of_struct1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array_of_struct1/test.desc +++ b/regression/cbmc-with-incr/equality_through_array_of_struct1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array_of_struct2/test.desc b/regression/cbmc-with-incr/equality_through_array_of_struct2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array_of_struct2/test.desc +++ b/regression/cbmc-with-incr/equality_through_array_of_struct2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array_of_struct3/test.desc b/regression/cbmc-with-incr/equality_through_array_of_struct3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array_of_struct3/test.desc +++ b/regression/cbmc-with-incr/equality_through_array_of_struct3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_array_of_struct4/test.desc b/regression/cbmc-with-incr/equality_through_array_of_struct4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_array_of_struct4/test.desc +++ b/regression/cbmc-with-incr/equality_through_array_of_struct4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct1/test.desc b/regression/cbmc-with-incr/equality_through_struct1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct1/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct2/test.desc b/regression/cbmc-with-incr/equality_through_struct2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct2/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct3/test.desc b/regression/cbmc-with-incr/equality_through_struct3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct3/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct4/test.desc b/regression/cbmc-with-incr/equality_through_struct4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct4/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct5/test.desc b/regression/cbmc-with-incr/equality_through_struct5/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct5/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct_containing_arrays1/test.desc b/regression/cbmc-with-incr/equality_through_struct_containing_arrays1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct_containing_arrays1/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct_containing_arrays1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct_containing_arrays2/test.desc b/regression/cbmc-with-incr/equality_through_struct_containing_arrays2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct_containing_arrays2/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct_containing_arrays2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_struct_containing_arrays3/test.desc b/regression/cbmc-with-incr/equality_through_struct_containing_arrays3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_struct_containing_arrays3/test.desc +++ b/regression/cbmc-with-incr/equality_through_struct_containing_arrays3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_union1/test.desc b/regression/cbmc-with-incr/equality_through_union1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_union1/test.desc +++ b/regression/cbmc-with-incr/equality_through_union1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_union2/test.desc b/regression/cbmc-with-incr/equality_through_union2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_union2/test.desc +++ b/regression/cbmc-with-incr/equality_through_union2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/equality_through_union3/test.desc b/regression/cbmc-with-incr/equality_through_union3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/equality_through_union3/test.desc +++ b/regression/cbmc-with-incr/equality_through_union3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/exit1/test.desc b/regression/cbmc-with-incr/exit1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/exit1/test.desc +++ b/regression/cbmc-with-incr/exit1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/extern_initialization1/test.desc b/regression/cbmc-with-incr/extern_initialization1/test.desc index 73b0a6abe16..eec83417ba2 100644 --- a/regression/cbmc-with-incr/extern_initialization1/test.desc +++ b/regression/cbmc-with-incr/extern_initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE file1.c file2.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/extern_initialization2/test.desc b/regression/cbmc-with-incr/extern_initialization2/test.desc index 8a09111c3b1..de55fd28989 100644 --- a/regression/cbmc-with-incr/extern_initialization2/test.desc +++ b/regression/cbmc-with-incr/extern_initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE file1.c file2.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/for-break1/test.desc b/regression/cbmc-with-incr/for-break1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/for-break1/test.desc +++ b/regression/cbmc-with-incr/for-break1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/for1/test.desc b/regression/cbmc-with-incr/for1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/for1/test.desc +++ b/regression/cbmc-with-incr/for1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/for2/test.desc b/regression/cbmc-with-incr/for2/test.desc index ae05c84a478..6b3369f42a1 100644 --- a/regression/cbmc-with-incr/for2/test.desc +++ b/regression/cbmc-with-incr/for2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/for3/test.desc b/regression/cbmc-with-incr/for3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/for3/test.desc +++ b/regression/cbmc-with-incr/for3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/function_option1/test.desc b/regression/cbmc-with-incr/function_option1/test.desc index 521d7365c2f..43cc7501c6e 100644 --- a/regression/cbmc-with-incr/function_option1/test.desc +++ b/regression/cbmc-with-incr/function_option1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --function f ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_c99-bool-1/test.desc b/regression/cbmc-with-incr/gcc_c99-bool-1/test.desc index d82c02459fc..1a11f07f85c 100644 --- a/regression/cbmc-with-incr/gcc_c99-bool-1/test.desc +++ b/regression/cbmc-with-incr/gcc_c99-bool-1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE c99-bool-1.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_conditional_expr1/test.desc b/regression/cbmc-with-incr/gcc_conditional_expr1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/gcc_conditional_expr1/test.desc +++ b/regression/cbmc-with-incr/gcc_conditional_expr1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_local_label1/test.desc b/regression/cbmc-with-incr/gcc_local_label1/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/gcc_local_label1/test.desc +++ b/regression/cbmc-with-incr/gcc_local_label1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/gcc_statement_expression1/test.desc b/regression/cbmc-with-incr/gcc_statement_expression1/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/gcc_statement_expression1/test.desc +++ b/regression/cbmc-with-incr/gcc_statement_expression1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_statement_expression2/test.desc b/regression/cbmc-with-incr/gcc_statement_expression2/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/gcc_statement_expression2/test.desc +++ b/regression/cbmc-with-incr/gcc_statement_expression2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_statement_expression3/test.desc b/regression/cbmc-with-incr/gcc_statement_expression3/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/gcc_statement_expression3/test.desc +++ b/regression/cbmc-with-incr/gcc_statement_expression3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_statement_expression4/test.desc b/regression/cbmc-with-incr/gcc_statement_expression4/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/gcc_statement_expression4/test.desc +++ b/regression/cbmc-with-incr/gcc_statement_expression4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_statement_expression5/test.desc b/regression/cbmc-with-incr/gcc_statement_expression5/test.desc index 9c96469df12..fb6666914d4 100644 --- a/regression/cbmc-with-incr/gcc_statement_expression5/test.desc +++ b/regression/cbmc-with-incr/gcc_statement_expression5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_vector1/test.desc b/regression/cbmc-with-incr/gcc_vector1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/gcc_vector1/test.desc +++ b/regression/cbmc-with-incr/gcc_vector1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/gcc_vector2/test.desc b/regression/cbmc-with-incr/gcc_vector2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/gcc_vector2/test.desc +++ b/regression/cbmc-with-incr/gcc_vector2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/goto1/test.desc b/regression/cbmc-with-incr/goto1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/goto1/test.desc +++ b/regression/cbmc-with-incr/goto1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/goto2/test.desc b/regression/cbmc-with-incr/goto2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/goto2/test.desc +++ b/regression/cbmc-with-incr/goto2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/goto3/test.desc b/regression/cbmc-with-incr/goto3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/goto3/test.desc +++ b/regression/cbmc-with-incr/goto3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/goto4/test.desc b/regression/cbmc-with-incr/goto4/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/goto4/test.desc +++ b/regression/cbmc-with-incr/goto4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/if1/test.desc b/regression/cbmc-with-incr/if1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/if1/test.desc +++ b/regression/cbmc-with-incr/if1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/if2/test.desc b/regression/cbmc-with-incr/if2/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/if2/test.desc +++ b/regression/cbmc-with-incr/if2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/if3/test.desc b/regression/cbmc-with-incr/if3/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/if3/test.desc +++ b/regression/cbmc-with-incr/if3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/if4/test.desc b/regression/cbmc-with-incr/if4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/if4/test.desc +++ b/regression/cbmc-with-incr/if4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/inline1/test.desc b/regression/cbmc-with-incr/inline1/test.desc index af20f90c655..b302e1734c3 100644 --- a/regression/cbmc-with-incr/inline1/test.desc +++ b/regression/cbmc-with-incr/inline1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c module.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/int-to-float1/test.desc b/regression/cbmc-with-incr/int-to-float1/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/int-to-float1/test.desc +++ b/regression/cbmc-with-incr/int-to-float1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/int-to-float2/test.desc b/regression/cbmc-with-incr/int-to-float2/test.desc index b7d95a28215..3d655761041 100644 --- a/regression/cbmc-with-incr/int-to-float2/test.desc +++ b/regression/cbmc-with-incr/int-to-float2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc-with-incr/locations1/test.desc b/regression/cbmc-with-incr/locations1/test.desc index 12c44d464cd..2521c59483c 100644 --- a/regression/cbmc-with-incr/locations1/test.desc +++ b/regression/cbmc-with-incr/locations1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --signed-overflow-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/noop1/test.desc b/regression/cbmc-with-incr/noop1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/noop1/test.desc +++ b/regression/cbmc-with-incr/noop1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/null1/test.desc b/regression/cbmc-with-incr/null1/test.desc index 376d43d5dfa..b7c95d95569 100644 --- a/regression/cbmc-with-incr/null1/test.desc +++ b/regression/cbmc-with-incr/null1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --no-simplify ^EXIT=0$ diff --git a/regression/cbmc-with-incr/null2/test.desc b/regression/cbmc-with-incr/null2/test.desc index 1d6654a4859..25a63f0fbdc 100644 --- a/regression/cbmc-with-incr/null2/test.desc +++ b/regression/cbmc-with-incr/null2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/offsetof1/test.desc b/regression/cbmc-with-incr/offsetof1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/offsetof1/test.desc +++ b/regression/cbmc-with-incr/offsetof1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc index 0d1e9fa0dba..0a7701cc8f6 100644 --- a/regression/cbmc-with-incr/pipe1/test.desc +++ b/regression/cbmc-with-incr/pipe1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --all-properties ^EXIT=10$ diff --git a/regression/cbmc-with-incr/realloc1/test.desc b/regression/cbmc-with-incr/realloc1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/realloc1/test.desc +++ b/regression/cbmc-with-incr/realloc1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/return1/test.desc b/regression/cbmc-with-incr/return1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/return1/test.desc +++ b/regression/cbmc-with-incr/return1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/return3/test.desc b/regression/cbmc-with-incr/return3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/return3/test.desc +++ b/regression/cbmc-with-incr/return3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/return4/test.desc b/regression/cbmc-with-incr/return4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/return4/test.desc +++ b/regression/cbmc-with-incr/return4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/return5/test.desc b/regression/cbmc-with-incr/return5/test.desc index 6de79559914..b9b38f2c4b4 100644 --- a/regression/cbmc-with-incr/return5/test.desc +++ b/regression/cbmc-with-incr/return5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/strtol1/test.desc b/regression/cbmc-with-incr/strtol1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/strtol1/test.desc +++ b/regression/cbmc-with-incr/strtol1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/strtol2/test.desc b/regression/cbmc-with-incr/strtol2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/strtol2/test.desc +++ b/regression/cbmc-with-incr/strtol2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/struct1/test.desc b/regression/cbmc-with-incr/struct1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/struct1/test.desc +++ b/regression/cbmc-with-incr/struct1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/struct3/test.desc b/regression/cbmc-with-incr/struct3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/struct3/test.desc +++ b/regression/cbmc-with-incr/struct3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/struct4/test.desc b/regression/cbmc-with-incr/struct4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/struct4/test.desc +++ b/regression/cbmc-with-incr/struct4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/struct6/test.desc b/regression/cbmc-with-incr/struct6/test.desc index da239c1965b..6550ede8bf0 100644 --- a/regression/cbmc-with-incr/struct6/test.desc +++ b/regression/cbmc-with-incr/struct6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --bounds-check --pointer-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/struct7/test.desc b/regression/cbmc-with-incr/struct7/test.desc index 96c9b4bcd7b..b1749fa8cd6 100644 --- a/regression/cbmc-with-incr/struct7/test.desc +++ b/regression/cbmc-with-incr/struct7/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-with-incr/struct8/test.desc b/regression/cbmc-with-incr/struct8/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/struct8/test.desc +++ b/regression/cbmc-with-incr/struct8/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/switch1/test.desc b/regression/cbmc-with-incr/switch1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/switch1/test.desc +++ b/regression/cbmc-with-incr/switch1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/switch2/test.desc b/regression/cbmc-with-incr/switch2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/switch2/test.desc +++ b/regression/cbmc-with-incr/switch2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/switch3/test.desc b/regression/cbmc-with-incr/switch3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/switch3/test.desc +++ b/regression/cbmc-with-incr/switch3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/switch4/test.desc b/regression/cbmc-with-incr/switch4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/switch4/test.desc +++ b/regression/cbmc-with-incr/switch4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/switch5/test.desc b/regression/cbmc-with-incr/switch5/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/switch5/test.desc +++ b/regression/cbmc-with-incr/switch5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/switch6/test.desc b/regression/cbmc-with-incr/switch6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/switch6/test.desc +++ b/regression/cbmc-with-incr/switch6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/union1/test.desc b/regression/cbmc-with-incr/union1/test.desc index 52168c7eba4..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/union1/test.desc +++ b/regression/cbmc-with-incr/union1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/union2/test.desc b/regression/cbmc-with-incr/union2/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/union2/test.desc +++ b/regression/cbmc-with-incr/union2/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/union3/test.desc b/regression/cbmc-with-incr/union3/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/union3/test.desc +++ b/regression/cbmc-with-incr/union3/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/union4/test.desc b/regression/cbmc-with-incr/union4/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/union4/test.desc +++ b/regression/cbmc-with-incr/union4/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/union5/test.desc b/regression/cbmc-with-incr/union5/test.desc index 33900ad2b78..4aa47233d39 100644 --- a/regression/cbmc-with-incr/union5/test.desc +++ b/regression/cbmc-with-incr/union5/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=10$ diff --git a/regression/cbmc-with-incr/union6/test.desc b/regression/cbmc-with-incr/union6/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/union6/test.desc +++ b/regression/cbmc-with-incr/union6/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/unsigned_char1/test.desc b/regression/cbmc-with-incr/unsigned_char1/test.desc index 0f995fec257..c61e9a874a1 100644 --- a/regression/cbmc-with-incr/unsigned_char1/test.desc +++ b/regression/cbmc-with-incr/unsigned_char1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c --unsigned-char ^EXIT=0$ diff --git a/regression/cbmc-with-incr/va_list1/test.desc b/regression/cbmc-with-incr/va_list1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/va_list1/test.desc +++ b/regression/cbmc-with-incr/va_list1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/va_list2/test.desc b/regression/cbmc-with-incr/va_list2/test.desc index 52168c7eba4..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/va_list2/test.desc +++ b/regression/cbmc-with-incr/va_list2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/void_ifthenelse/test.desc b/regression/cbmc-with-incr/void_ifthenelse/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/void_ifthenelse/test.desc +++ b/regression/cbmc-with-incr/void_ifthenelse/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$ diff --git a/regression/cbmc-with-incr/while1/test.desc b/regression/cbmc-with-incr/while1/test.desc index 9efefbc7362..aea17ee4da8 100644 --- a/regression/cbmc-with-incr/while1/test.desc +++ b/regression/cbmc-with-incr/while1/test.desc @@ -1,4 +1,4 @@ -CORE +FUTURE main.c ^EXIT=0$