More tests adjusted

Author: NlightNFotis

regression/cbmc/Float-div2/test.desc

@@ -1,6 +1,6 @@
 CORE broken-z3-smt-backend no-new-smt
 main.c
---floatbv
+--floatbv --no-built-in-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Float-div3/test.desc

@@ -1,6 +1,6 @@
 CORE broken-z3-smt-backend no-new-smt
 main.c
---floatbv
+--floatbv --no-built-in-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Malloc11/test.desc

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

regression/cbmc/Pointer_byte_extract2/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILURE$
-^\*\* 1 of 2 failed 
+^\*\* 2 of 4 failed
 --
 ^warning: ignoring

regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -1,6 +1,6 @@
 CORE paths-lifo-expected-failure
 test.c
---cover location --pointer-check --malloc-may-fail --malloc-fail-null
+--cover location --malloc-may-fail --malloc-fail-null
 \[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
 \[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED
 \[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED

regression/cbmc/cover-failed-assertions/test.desc

@@ -1,6 +1,6 @@
 CORE paths-lifo-expected-failure
 test.c
---cover location --cover-failed-assertions --pointer-check --malloc-may-fail --malloc-fail-null
+--cover location --cover-failed-assertions --malloc-may-fail --malloc-fail-null
 \[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
 \[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): SATISFIED
 \[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED

regression/cbmc/coverage_report2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---symex-coverage-report - --unwind 1
+--symex-coverage-report - --unwind 1 --unwinding-assertions
 <line branch="true" condition-coverage="50% \(1/2\)" hits="2" number="3">
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/export-symex-ready-goto/exported.symex.ready.goto

@@ -6,7 +6,9 @@ main.c
 ^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
 ^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
 ^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$
-^\*\* 5 of \d+ failed
+^\[main\.overflow\.6\] line 20 arithmetic overflow on signed \+ in n \+ n: FAILURE$
+^\[main\.overflow\.7\] line 21 arithmetic overflow on signed \+ in x \+ n: FAILURE$
+^\*\* 7 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$