diff --git a/regression/cbmc-incr-oneloop/alarm1/test.desc b/regression/cbmc-incr-oneloop/alarm1/test.desc index 87b0754ad15..b0164719dbb 100644 --- a/regression/cbmc-incr-oneloop/alarm1/test.desc +++ b/regression/cbmc-incr-oneloop/alarm1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-max 15 +--no-standard-checks --incremental-loop main.0 --unwind-max 15 activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-incr-oneloop/arrays5/test.desc b/regression/cbmc-incr-oneloop/arrays5/test.desc index 2ce7fd6f126..a10b7283faa 100644 --- a/regression/cbmc-incr-oneloop/arrays5/test.desc +++ b/regression/cbmc-incr-oneloop/arrays5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-max 5 --arrays-uf-always +--no-standard-checks --incremental-loop main.0 --unwind-max 5 --arrays-uf-always ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/cruise1/test.desc b/regression/cbmc-incr-oneloop/cruise1/test.desc index 19e1f90f4c4..e42fcabb182 100644 --- a/regression/cbmc-incr-oneloop/cruise1/test.desc +++ b/regression/cbmc-incr-oneloop/cruise1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-max 10 +--no-standard-checks --incremental-loop main.0 --unwind-max 10 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc index 72879e32fe5..f6348e82931 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind-min 2 --unwind-max 4 --incremental-loop main.0 +--no-standard-checks --unwind-min 2 --unwind-max 4 --incremental-loop main.0 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc index c52e8ccd2bb..a6f44007b7e 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind-min 6 --unwind-max 8 --incremental-loop main.0 --ignore-properties-before-unwind-min +--no-standard-checks --unwind-min 6 --unwind-max 8 --incremental-loop main.0 --ignore-properties-before-unwind-min ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/no-asserts/test.desc b/regression/cbmc-incr-oneloop/no-asserts/test.desc index a5c2f27a5d6..4e297be474c 100644 --- a/regression/cbmc-incr-oneloop/no-asserts/test.desc +++ b/regression/cbmc-incr-oneloop/no-asserts/test.desc @@ -1,6 +1,6 @@ CORE test.c ---incremental-loop main.0 +--no-standard-checks --incremental-loop main.0 activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc b/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc index fb2b8088599..b63b0307dbe 100644 --- a/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc +++ b/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind-max 10 --incremental-loop main.0 +--no-standard-checks --unwind-max 10 --incremental-loop main.0 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/simplifier1/test.desc b/regression/cbmc-incr-oneloop/simplifier1/test.desc index 709e207fdab..f58a144ab30 100644 --- a/regression/cbmc-incr-oneloop/simplifier1/test.desc +++ b/regression/cbmc-incr-oneloop/simplifier1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-max 5 +--no-standard-checks --incremental-loop main.0 --unwind-max 5 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/simplifier2/test.desc b/regression/cbmc-incr-oneloop/simplifier2/test.desc index 3ad5bec6bce..74b0ad73a1e 100644 --- a/regression/cbmc-incr-oneloop/simplifier2/test.desc +++ b/regression/cbmc-incr-oneloop/simplifier2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-max 3 --stop-on-fail +--no-standard-checks --incremental-loop main.0 --unwind-max 3 --stop-on-fail ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$