[DO NOT REVIEW] [DO NOT MERGE] add --no-standard-checks to all CORE tests

regression/acceleration/array_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/array_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/array_safe3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/array_safe4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/const_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/diamond_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/diamond_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/diamond_unsafe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions
+--no-standard-checks --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/acceleration/functions_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/multivar_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/multivar_unsafe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions
+--no-standard-checks --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/acceleration/nested_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/overflow_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/phases_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_safe4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/simple_unsafe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions
+--no-standard-checks --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/acceleration/simple_unsafe3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions
+--no-standard-checks --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/acceleration/underapprox_safe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_safe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_unsafe1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/acceleration/underapprox_unsafe2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/book-examples/abs/C1.desc

@@ -1,6 +1,6 @@
 CORE
 abs.c
---function abs
+--no-standard-checks --function abs
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/book-examples/abs/C13.desc

@@ -1,5 +1,5 @@
 CORE
 abs.c
---function abs --signed-overflow-check --show-goto-functions
+--no-standard-checks --function abs --signed-overflow-check --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$

regression/book-examples/abs/C2.desc

@@ -1,6 +1,6 @@
 CORE
 abs.c
---function abs --signed-overflow-check
+--no-standard-checks --function abs --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/book-examples/abs/C3.desc

@@ -1,6 +1,6 @@
 CORE
 abs.c
---function abs --signed-overflow-check --trace
+--no-standard-checks --function abs --signed-overflow-check --trace
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/book-examples/binsearch/C4.desc

@@ -1,6 +1,6 @@
 CORE
 binsearch.c
---function binsearch --unwind 6 --bounds-check --unwinding-assertions
+--no-standard-checks --function binsearch --unwind 6 --bounds-check --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

regression/book-examples/lock/depth.desc

@@ -1,6 +1,6 @@
 CORE
 lock.c
---depth 10
+--no-standard-checks --depth 10
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/book-examples/lock/unwind1.desc

@@ -1,6 +1,6 @@
 CORE
 lock.c
---unwind 1
+--no-standard-checks --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/book-examples/lock/unwind2.desc

@@ -1,6 +1,6 @@
 CORE
 lock.c
---unwind 2
+--no-standard-checks --unwind 2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/book-examples/login/C5.desc

@@ -1,6 +1,6 @@
 CORE
 login.c
---unwind 20 --bounds-check
+--no-standard-checks --unwind 20 --bounds-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/book-examples/login/C6.desc

@@ -1,6 +1,6 @@
 CORE
 login.c
---show-properties --bounds-check --pointer-check
+--no-standard-checks --show-properties --bounds-check --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 Property main\.array_bounds\.\d

regression/book-examples/login/C7.desc

@@ -1,5 +1,5 @@
 CORE
 login.c
---unwind 20 --show-vcc --bounds-check --pointer-check
+--no-standard-checks --unwind 20 --show-vcc --bounds-check --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$

regression/book-examples/login/C8.desc

@@ -1,6 +1,6 @@
 CORE
 login.c
---unwind 20 --bounds-check --pointer-check
+--no-standard-checks --unwind 20 --bounds-check --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/book-examples/login/C9.desc

@@ -1,6 +1,6 @@
 CORE
 login.c
---unwind 20 --bounds-check --pointer-check --trace
+--no-standard-checks --unwind 20 --bounds-check --pointer-check --trace
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/book-examples/pid/C11.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 pid.c
---cover mcdc --unwind 6
+--no-standard-checks --cover mcdc --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
 coverage results

regression/cbmc-concurrency/array1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/assume1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-concurrency/assume2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/atomic_section_sc1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/atomic_section_sc2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/atomic_section_sc3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/atomic_section_sc4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/atomic_section_sc5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-concurrency/atomic_section_sc6/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=6$
 ^SIGNAL=0$
 ^spawning threads out of atomic sections is not allowed

regression/cbmc-concurrency/atomic_section_sc7/test-guard.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---program-only
+--no-standard-checks --program-only
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-concurrency/atomic_section_sc7/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-concurrency/conditional_spawn1/test.desc

@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$