Fixed cbmc-incr-oneloop test failing unwinding assertions

diffblue · Dec 14, 2023 · fd57e6a · fd57e6a
1 parent 2f1eb7c
commit fd57e6a
Show file tree

Hide file tree

Showing 9 changed files with 9 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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$