Adjust default flags in regression/cbmc tests.

Author: NlightNFotis

regression/cbmc/ACSL/operators.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 operators.c
-
+--no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Address_of1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---stop-on-fail
+--stop-on-fail --no-pointer-check
 ^\[main\.assertion
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Anonymous_Struct1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Array_UF21/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---arrays-uf-always --bounds-check
+--arrays-uf-always
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Array_operations1/full-slice.desc

@@ -10,9 +10,9 @@ main.c
 ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
-^\*\* 5 of 15 failed
+^\*\* 5 of 19 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
 --
-Verify the properties of various cprover array primitves
+Verify the properties of various CPROVER array primitives.

regression/cbmc/Array_operations1/test.desc

@@ -10,7 +10,7 @@ main.c
 ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
-^\*\* 5 of 15 failed
+^\*\* 5 of 19 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Associativity1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/BV_Arithmetic3/test.desc

@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$)
+(Starting CEGAR Loop|^Generated 68 VCC\(s\), 0 remaining after simplification$)
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc/BV_Arithmetic4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
- --unwind 32
+ --unwind 32 --no-signed-overflow-check --no-undefined-shift-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Bitfields3/paths.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---pointer-check --bounds-check --paths lifo
+--paths lifo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$