Merge pull request #8051 from esteffin/esteffin/add-cbmc-regression-to-incremental-smt

Enable all `cbmc` regression tests that are passing to run with new SMT backend

Author: Enrico Steffinlongo

regression/cbmc/Array_UF21/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --arrays-uf-always --bounds-check
 ^VERIFICATION FAILED$

regression/cbmc/Float-equality2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 (Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)

regression/cbmc/Float-overflow1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv --float-overflow-check
 ^EXIT=0$

regression/cbmc/Float-overflow2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv --float-overflow-check
 ^EXIT=10$

regression/cbmc/Float-rounding/compile_time_rounding.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 compile_time_rounding.c
 
 ^EXIT=0$

regression/cbmc/Float1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float11/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float13/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Float14/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Float2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float22/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float7/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Function5/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --pointer-check --bounds-check
 ^SIGNAL=0$

regression/cbmc/Function_Pointer11/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Function_Pointer15/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/Function_Pointer2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Function_Pointer3/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Function_Pointer6/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Function_Pointer9/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --function foo
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$

regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --function foo
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$

regression/cbmc/Initialization5/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/Linking7/member-name-mismatch.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 module2.c
 ^EXIT=10$

regression/cbmc/Linking7/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 module.c
 ^EXIT=10$

regression/cbmc/Malloc19/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Malloc8/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/Memory_leak1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --memory-leak-check
 ^EXIT=10$

regression/cbmc/Memory_leak2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --memory-leak-check
 ^EXIT=0$

regression/cbmc/Pointer14/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --pointer-check
 ^VERIFICATION FAILED$

regression/cbmc/Pointer2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Pointer27/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^SIGNAL=0$

regression/cbmc/Pointer_comparison4/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --unwind 10 --unwinding-assertions
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Pointer_comparison5/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^Generated \d+ VCC\(s\), 1 remaining after simplification$

regression/cbmc/String2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=10$

regression/cbmc/String8/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc/String_Abstraction13/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 constant.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/String_Abstraction16/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 ptr-arith.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/String_Abstraction17/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 strcpy-no-decl.c
 --string-abstraction --validate-goto-model
 ^EXIT=10$

regression/cbmc/String_Abstraction18/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 strcpy.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/String_Abstraction21/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 strcpy2.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/String_Abstraction4/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --string-abstraction --pointer-check --bounds-check
 ^EXIT=10$

regression/cbmc/String_Abstraction5/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --string-abstraction --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc/String_Literal1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --trace
 ^State \d+ file main.c function main line 20 thread 0$

regression/cbmc/array-cell-sensitivity1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[1\]\] =

regression/cbmc/array-cell-sensitivity10/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[0\]\]..x =

regression/cbmc/array-cell-sensitivity10/test_execution.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/array-cell-sensitivity11/test_execution.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/array-cell-sensitivity3/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[0\]\] =

regression/cbmc/array-cell-sensitivity3/test_execution.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/array-cell-sensitivity4/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[1\]\] =

regression/cbmc/array-cell-sensitivity5/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 symex_dynamic::dynamic_object#2\[\[1\]\] =

regression/cbmc/array-cell-sensitivity6/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 symex_dynamic::dynamic_object#2\[\[1\]\] =

regression/cbmc/array-cell-sensitivity7/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[1\]\] =

regression/cbmc/array-cell-sensitivity7/test_execution.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/array-cell-sensitivity8/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[1\]\] =

regression/cbmc/array-cell-sensitivity8/test_execution.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/atomic_section_seq1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/byte_update11/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update14/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/compact-trace/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --compact-trace
 activate-multi-line-match

regression/cbmc/complex1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/constructor2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/coverage_report2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --symex-coverage-report - --unwind 1
 <line branch="true" condition-coverage="50% \(1/2\)" hits="2" number="3">

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
 \{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$0\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)

regression/cbmc/empty_compound_type4/test.desc

@@ -1,4 +1,4 @@
-CORE gcc-only no-new-smt
+CORE gcc-only
 main.c
 --trace
 ^VERIFICATION FAILED$

regression/cbmc/enum5/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$