enable 130 SMT2 tests that now pass

Author: kroening

scripts/delete_failing_smt2_solver_tests

@@ -1,43 +1,25 @@
 #!/bin/sh
 
 cd regression/cbmc
-rm ACSL/operators.desc
 rm Address_of2/test.desc
 rm Anonymous_Struct3/test.desc
 rm Array_Initialization2/test.desc
 rm Array_operations1/test.desc
-rm Assumption1/test.desc
-rm BV_Arithmetic1/test.desc
 rm BV_Arithmetic6/test.desc
 rm Bitfields1/test.desc
 rm Bitfields3/test.desc
-rm Bool1/test.desc
-rm Bool2/test.desc
-rm Bool3/test.desc
-rm Boolean_Guards1/test.desc
-rm Computed-Goto1/test.desc
 rm Division2/test.desc
 rm Double-to-float-no-simp1/test.desc
 rm Double-to-float-no-simp1-fix1/test.desc
 rm Double-to-float-no-simp1-fix2/test.desc
-rm Ellipsis2/test.desc
 rm Empty_struct1/test.desc
-rm Endianness1/test.desc
-rm Endianness2/test.desc
 rm Endianness3/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc
 rm Endianness7/test.desc
-rm Endianness8/test.desc
-rm Error_Label1/test.desc
-rm Error_Label2/test.desc
-rm Error_Label3/test.desc
-rm Eval_Order1/test.desc
-rm Failing_Assert1/test.desc
 rm Fixedbv3/test.desc
 rm Fixedbv5/test.desc
 rm Fixedbv6/test.desc
-rm Fixedbv8/test.desc
 rm Float-Rounding1/test.desc
 rm Float-div1/test.desc
 rm Float-div2/test.desc
@@ -53,7 +35,6 @@ rm Float-no-simp6/test.desc
 rm Float-no-simp7/test.desc
 rm Float-no-simp8/test.desc
 rm Float-no-simp9/test.desc
-rm Float-overflow2/test.desc
 rm Float-smt2-1/test.desc
 rm Float-to-double1/test.desc
 rm Float-to-double2/test.desc
@@ -74,68 +55,31 @@ rm Float4/test.desc
 rm Float5/test.desc
 rm Float6/test.desc
 rm Float8/test.desc
-rm Free1/test.desc
 rm Free2/test.desc
-rm Free3/test.desc
-rm Free4/test.desc
 rm Function1/test.desc
-rm Function2/test.desc
-rm Function5/test.desc
-rm Function8/test.desc
-rm Function9/test.desc
-rm Function_Eval_Order2/test.desc
-rm Function_Pointer15/test.desc
-rm Function_Pointer2/test.desc
 rm Function_Pointer3/test.desc
-rm Function_Pointer6/test.desc
-rm Function_Pointer8/test.desc
-rm Function_Pointer9/test.desc
-rm Initialization5/test.desc
-rm Initialization6/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
-rm Linking8/test.desc
-rm Local_out_of_scope1/test.desc
-rm Local_out_of_scope2/test.desc
-rm Local_out_of_scope3/test.desc
-rm Malloc15/test.desc
 rm Malloc17/test.desc
 rm Malloc18/test.desc
 rm Malloc19/test.desc
 rm Malloc20/test.desc
-rm Malloc21/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memmove1/test.desc
 rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
-rm Mod1/test.desc
-rm Mod2/test.desc
-rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
-rm Multi_Dimensional_Array3/test.desc
 rm Multi_Dimensional_Array4/test.desc
 rm Multi_Dimensional_Array6/test.desc
 rm Multiple_Properties1/test.desc
-rm Negation2/test.desc
-rm Overflow_Addition1/test.desc
 rm Overflow_Leftshift1/test.desc
-rm Overflow_Multiplication1/test.desc
 rm Overflow_Subtraction1/test.desc
-rm Pointer_Arithmetic1/test.desc
 rm Pointer_Arithmetic10/test.desc
 rm Pointer_Arithmetic11/test.desc
 rm Pointer_Arithmetic12/test.desc
-rm Pointer_Arithmetic5/test.desc
 rm Pointer_Arithmetic6/test.desc
-rm Pointer_Arithmetic8/test.desc
-rm Pointer_array1/test.desc
-rm Pointer_array2/test.desc
-rm Pointer_array3/test.desc
-rm Pointer_array4/test.desc
 rm Pointer_array5/test.desc
-rm Pointer_array6/test.desc
-rm Pointer_byte_extract1/test.desc
 rm Pointer_byte_extract2/test.desc
 rm Pointer_byte_extract3/test.desc
 rm Pointer_byte_extract4/test.desc
@@ -158,30 +102,19 @@ rm Quantifiers-not-exists/test.desc
 rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
 rm Quantifiers1/test.desc
-rm Recursion4/test.desc
 rm Recursion5/test.desc
-rm Sideeffects5/test.desc
-rm Sideeffects6/test.desc
-rm String2/test.desc
 rm String6/test.desc
 rm Struct_Bytewise1/test.desc
 rm Struct_Bytewise2/test.desc
 rm Struct_Initialization2/test.desc
-rm Struct_Initialization5/test.desc
 rm Struct_Padding1/test.desc
-rm Typecast1/test.desc
-rm Typecast2/test.desc
-rm Undefined_Function1/test.desc
-rm Undefined_Function2/test.desc
 rm Undefined_Shift1/test.desc
 rm Union_Initialization1/test.desc
 rm Unwinding_Locality1/test.desc
-rm abs1/test.desc
 rm address_space_size_limit1/test.desc
 rm address_space_size_limit3/test.desc
 rm argv1/test.desc
 rm array-tests/test.desc
-rm atomic_section_seq1/test.desc
 rm big-endian-array1/test.desc
 rm bounds_check1/test.desc
 rm byte_update1/test.desc
@@ -191,16 +124,8 @@ rm byte_update4/test.desc
 rm byte_update5/test.desc
 rm byte_update6/test.desc
 rm byte_update7/test.desc
-rm byte_update8/test.desc
-rm byte_update9/test.desc
-rm c99_Bool/test.desc
-rm cprover_bool1/test.desc
-rm divide-by-one-simplify/test.desc
 rm dynamic_size1/stack_object.desc
 rm dynamic_size1/test.desc
-rm dynamic_sizeof1/test.desc
-rm enum3/test.desc
-rm enum5/test.desc
 rm equality_through_array1/test.desc
 rm equality_through_array2/test.desc
 rm equality_through_array3/test.desc
@@ -211,108 +136,59 @@ rm equality_through_array_of_struct1/test.desc
 rm equality_through_array_of_struct2/test.desc
 rm equality_through_array_of_struct3/test.desc
 rm equality_through_array_of_struct4/test.desc
-rm equality_through_struct1/test.desc
-rm equality_through_struct2/test.desc
-rm equality_through_struct3/test.desc
-rm equality_through_struct4/test.desc
-rm equality_through_struct5/test.desc
 rm equality_through_struct_containing_arrays1/test.desc
 rm equality_through_struct_containing_arrays2/test.desc
 rm equality_through_struct_containing_arrays3/test.desc
 rm equality_through_union1/test.desc
 rm equality_through_union2/test.desc
 rm equality_through_union3/test.desc
-rm exit1/test.desc
-rm extern_initialization1/test.desc
 rm fgets1/test.desc
-rm for2/test.desc
 rm full_slice1/test.desc
 rm full_slice2/test.desc
 rm gcc_bswap1/test.desc
-rm gcc_c99-bool-1/test.desc
-rm gcc_local_label1/test.desc
-rm gcc_popcount1/test.desc
 rm gcc_statement_expression4/test.desc
 rm gcc_switch_case_range1/test.desc
 rm gcc_switch_case_range2/test.desc
 rm gcc_vector1/test.desc
 rm gcc_vector2/test.desc
-rm getenv-overflow1/test.desc
-rm goto1/test.desc
-rm goto2/test.desc
-rm goto4/test.desc
-rm goto5/test.desc
 rm graphml_witness1/test.desc
 rm havoc_object1/test.desc
 rm hex_trace/test.desc
-rm if1/test.desc
 rm if2/test.desc
-rm if3/test.desc
-rm if4/test.desc
 rm inet_endian1/test.desc
 rm int-to-float2/test.desc
 rm integer-assignments1/test.desc
-rm json1/test.desc
 rm little-endian-array1/test.desc
-rm member1/test.desc
-rm memcpy1/test.desc
-rm memcpy2/test.desc
-rm memcpy3/test.desc
 rm memory_allocation1/test.desc
-rm memset1/test.desc
 rm memset3/test.desc
 rm mm_io1/test.desc
 rm no_nondet_static/test.desc
-rm null1/test.desc
-rm null2/test.desc
-rm path-per-path-vccs/test.desc
 rm pipe1/test.desc
-rm pointer-extra-checks/test.desc
 rm pointer-function-parameters/test.desc
 rm pointer-function-parameters-2/test.desc
-rm posix_memalign/test.desc
-rm printf1/test.desc
 rm read1/test.desc
 rm realloc1/test.desc
 rm realloc2/test.desc
-rm return2/test.desc
-rm return5/test.desc
 rm scanf1/test.desc
-rm self_loops_to_assumptions1/no-assume.desc
 rm simple_assert/test.desc
 rm stack-trace/test.desc
 rm strcat1/test.desc
-rm struct1/test.desc
 rm struct10/test.desc
-rm struct3/test.desc
 rm struct6/test.desc
 rm struct7/test.desc
-rm struct8/test.desc
 rm struct9/test.desc
-rm switch1/test.desc
-rm switch2/test.desc
-rm switch3/test.desc
-rm switch4/test.desc
-rm switch5/test.desc
-rm trace_address_arithmetic1/test.desc
 rm trace-values/trace-values.desc
-rm trace_options_json_extended/extended.desc
-rm trace_options_json_extended/non-extended.desc
-rm trace_show_code/test.desc
+rm trace_address_arithmetic1/test.desc
 rm trace_show_function_calls/test.desc
 rm uncaught_exceptions_analysis1/test.desc
 rm uniform_array1/test.desc
 rm union11/union_list.desc
-rm union3/test.desc
 rm union5/test.desc
 rm union6/test.desc
 rm union7/test.desc
 rm union8/test.desc
 rm union9/test.desc
 rm unsigned___int128/test.desc
-rm unwind_counters2/test.desc
-rm unwind_counters3/test.desc
-rm variable-access-to-constant-array/test.desc
 rm void_pointer2/test.desc
 rm void_pointer3/test.desc
 rm while1/test.desc