Merge pull request #8106 from esteffin/esteffin/fixing-tests-new-default-checks

Run again tests with new default checks

Author: Enrico Steffinlongo

regression/acceleration/accelerate.sh

@@ -16,7 +16,7 @@ is_windows=$4
 shift 4
 
 cfile=""
-cbmcargs="--no-standard-checks"
+cbmcargs=""
 
 # create the temporary directory relative to the current directory, thus
 # avoiding file names that start with a "/", which confuses goto-cl (Windows)

regression/acceleration/array_safe1/test.desc

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

regression/acceleration/array_safe2/test.desc

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

regression/acceleration/array_safe3/test.desc

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

regression/acceleration/array_safe4/test.desc

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

regression/acceleration/const_safe1/test.desc

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

regression/acceleration/diamond_safe1/test.desc

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

regression/acceleration/diamond_safe2/test.desc

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

regression/acceleration/functions_safe1/test.desc

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

regression/acceleration/multivar_safe1/test.desc

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