Source: cbmc Version: 5.95.1-4 Severity: serious Justification: FTBFS Tags: trixie sid ftbfs User: lu...@debian.org Usertags: ftbfs-20240420 ftbfs-trixie ftbfs-t64-armhf
Hi, During a rebuild of all packages in sid, your package failed to build on armhf. Relevant part (hopefully): > make[4]: Entering directory '/<<PKGBUILDDIR>>/regression/cbmc' > Makefile:40: warning: overriding recipe for target 'clean' > ../../src/common:246: warning: ignoring old recipe for target 'clean' > Loading > 1114 tests found > > Running tests > Running ACSL/operators.desc [[32mOK[0m] in 0 seconds > Running ACSL/quantifier-precedence.desc [[32mOK[0m] in 0 seconds > Running ASHR1/test.desc [[32mOK[0m] in 0 seconds > Running Address_of1/test.desc [[32mOK[0m] in 0 seconds > Running Address_of2/test.desc [[32mOK[0m] in 0 seconds > Running Anonymous_Struct1/test.desc [[32mOK[0m] in 1 seconds > Running Anonymous_Struct2/test.desc [[32mOK[0m] in 0 seconds > Running Anonymous_Struct3/test.desc [[32mOK[0m] in 0 seconds > Running Array_Access1/test.desc [[32mOK[0m] in 0 seconds > Running Array_Access2/test.desc [[32mOK[0m] in 0 seconds > Running Array_Access3/test.desc [[32mOK[0m] in 0 seconds > Running Array_Initialization1/test.desc [[32mOK[0m] in 0 seconds > Running Array_Initialization2/test.desc [[32mOK[0m] in 0 seconds > Running Array_Initialization3/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer1/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer2/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer3/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer4/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer5/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer6/test.desc [[32mOK[0m] in 0 seconds > Running Array_Pointer7/test.desc [[32mOK[0m] in 0 seconds > Running Array_Propagation1/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF1/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF10/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF11/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF12/test.desc [[32mOK[0m] in 1 seconds > Running Array_UF13/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF14/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF15/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF16/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF17/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF18/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF19/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF2/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF20/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF21/test.desc [[32mOK[0m] in 1 seconds > Running Array_UF22/test.desc [SKIPPED] > Running Array_UF3/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF4/test.desc [SKIPPED] > Running Array_UF5/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF6/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF7/test.desc [[32mOK[0m] in 0 seconds > Running Array_UF8/test.desc [SKIPPED] > Running Array_UF9/test.desc [[32mOK[0m] in 0 seconds > Running Array_operations1/full-slice.desc [[32mOK[0m] in 0 seconds > Running Array_operations1/test.desc [[32mOK[0m] in 0 seconds > Running Array_operations2/test.desc [[32mOK[0m] in 0 seconds > Running Associativity1/test.desc [[32mOK[0m] in 0 seconds > Running Assumption1/test.desc [[32mOK[0m] in 0 seconds > Running BV_Arithmetic1/test.desc [[32mOK[0m] in 1 seconds > Running BV_Arithmetic2/test.desc [[32mOK[0m] in 0 seconds > Running BV_Arithmetic3/test.desc [[32mOK[0m] in 0 seconds > Running BV_Arithmetic4/test.desc [[32mOK[0m] in 0 seconds > Running BV_Arithmetic5/test.desc [[32mOK[0m] in 0 seconds > Running BV_Arithmetic6/test.desc [[32mOK[0m] in 0 seconds > Running Bitfields1/test.desc [[32mOK[0m] in 0 seconds > Running Bitfields2/test.desc [[32mOK[0m] in 0 seconds > Running Bitfields3/paths.desc [[32mOK[0m] in 1 seconds > Running Bitfields3/test.desc [[32mOK[0m] in 0 seconds > Running Bitfields4/test.desc [[32mOK[0m] in 0 seconds > Running Bool/bool1.desc [[32mOK[0m] in 0 seconds > Running Bool/bool2.desc [[32mOK[0m] in 0 seconds > Running Bool/bool3.desc [[32mOK[0m] in 0 seconds > Running Bool/bool4.desc [[32mOK[0m] in 0 seconds > Running Bool/bool5-full-slice.desc [[32mOK[0m] in 0 seconds > Running Bool/bool5.desc [[32mOK[0m] in 0 seconds > Running Bool/bool6.desc [[32mOK[0m] in 1 seconds > Running Bool/bool7.desc [SKIPPED] > Running Boolean_Guards1/test.desc [[32mOK[0m] in 0 seconds > Running Computed-Goto1/test.desc [[32mOK[0m] in 0 seconds > Running Division1/test.desc [[32mOK[0m] in 0 seconds > Running Division2/test.desc [[32mOK[0m] in 0 seconds > Running Ellipsis1/test.desc [[32mOK[0m] in 0 seconds > Running Ellipsis2/test.desc [[32mOK[0m] in 0 seconds > Running Empty_struct1/test.desc [[32mOK[0m] in 0 seconds > Running Empty_struct2/test.desc [[32mOK[0m] in 0 seconds > Running Empty_struct3/test.desc [[32mOK[0m] in 0 seconds > Running End_thread1/test.desc [[32mOK[0m] in 0 seconds > Running Endianness1/test.desc [[32mOK[0m] in 0 seconds > Running Endianness2/test.desc [[32mOK[0m] in 0 seconds > Running Endianness3/test.desc [[32mOK[0m] in 0 seconds > Running Endianness4/test.desc [[32mOK[0m] in 0 seconds > Running Endianness5/test.desc [[32mOK[0m] in 0 seconds > Running Endianness6/test.desc [[32mOK[0m] in 0 seconds > Running Endianness7/test.desc [[32mOK[0m] in 0 seconds > Running Endianness8/test.desc [[32mOK[0m] in 0 seconds > Running Endianness9/test.desc [[32mOK[0m] in 0 seconds > Running Error_Label1/test.desc [[32mOK[0m] in 0 seconds > Running Error_Label2/test.desc [[32mOK[0m] in 0 seconds > Running Error_Label3/test.desc [[32mOK[0m] in 0 seconds > Running Eval_Order1/test.desc [[32mOK[0m] in 0 seconds > Running Eval_Order2/test.desc [SKIPPED] > Running Exceptions1/test.desc [[32mOK[0m] in 1 seconds > Running Failed_Symbols1/test.desc [[32mOK[0m] in 0 seconds > Running Failing_Assert1/dimacs.desc [[32mOK[0m] in 0 seconds > Running Failing_Assert1/external-z3.desc [[32mOK[0m] in 0 seconds > Running Failing_Assert1/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv1/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv2/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv3/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv4/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv5/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv6/test.desc [[32mOK[0m] in 0 seconds > Running Fixedbv7/test.desc [SKIPPED] > Running Fixedbv8/test.desc [[32mOK[0m] in 0 seconds > Running Float-div2/test.desc [[32mOK[0m] in 0 seconds > Running Float-div3/test.desc [[32mOK[0m] in 0 seconds > Running Float-equality1/test_equality.desc [SKIPPED] > Running Float-equality1/test_no_equality.desc [[32mOK[0m] in 0 seconds > Running Float-equality2/test.desc [[32mOK[0m] in 0 seconds > Running Float-flags-no-simp1/test.desc [[32mOK[0m] in 1 seconds > Running Float-flags-simp1/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp1/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp2/test.desc [[32mOK[0m] in 2 seconds > Running Float-no-simp3/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp4/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp5/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp6/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp7/test.desc [[32mOK[0m] in 0 seconds > Running Float-no-simp9/test.desc [[32mOK[0m] in 0 seconds > Running Float-overflow1/test.desc [[32mOK[0m] in 0 seconds > Running Float-overflow2/test.desc [[32mOK[0m] in 0 seconds > Running Float-rounding/compile_time_rounding.desc [[32mOK[0m] in 0 > seconds > Running Float-rounding2/test.desc [[32mOK[0m] in 0 seconds > Running Float-smt2-1/test.desc [SKIPPED] > Running Float-to-double2/test.desc [[32mOK[0m] in 1 seconds > Running Float-to-int1/test.desc [[32mOK[0m] in 0 seconds > Running Float-to-int2/test.desc [[32mOK[0m] in 0 seconds > Running Float-to-int3/test.desc [[32mOK[0m] in 0 seconds > Running Float-zero-sum1/test.desc [[32mOK[0m] in 0 seconds > Running Float1/test.desc [[32mOK[0m] in 0 seconds > Running Float11/test.desc [[32mOK[0m] in 0 seconds > Running Float12/test.desc [[32mOK[0m] in 0 seconds > Running Float13/test.desc [[32mOK[0m] in 0 seconds > Running Float14/test.desc [[32mOK[0m] in 0 seconds > Running Float2/test.desc [[32mOK[0m] in 0 seconds > Running Float20/test.desc [[32mOK[0m] in 0 seconds > Running Float21/test.desc [[32mOK[0m] in 1 seconds > Running Float22/test.desc [[32mOK[0m] in 0 seconds > Running Float23/test.desc [[32mOK[0m] in 0 seconds > Running Float24/test.desc [[32mOK[0m] in 0 seconds > Running Float3/test.desc [[32mOK[0m] in 0 seconds > Running Float4/test.desc [[32mOK[0m] in 8 seconds > Running Float5/test.desc [[32mOK[0m] in 0 seconds > Running Float6/test.desc [[32mOK[0m] in 0 seconds > Running Float7/test.desc [[32mOK[0m] in 0 seconds > Running Float8/smt.desc [SKIPPED] > Running Float8/test.desc [[32mOK[0m] in 0 seconds > Running Free1/test.desc [[32mOK[0m] in 0 seconds > Running Free2/test.desc [[32mOK[0m] in 0 seconds > Running Free3/test.desc [[32mOK[0m] in 0 seconds > Running Free4/test.desc [[32mOK[0m] in 1 seconds > Running Function-KnR1/test.desc [[32mOK[0m] in 0 seconds > Running Function1/test.desc [[32mOK[0m] in 0 seconds > Running Function10/test.desc [[32mOK[0m] in 0 seconds > Running Function11/test.desc [[32mOK[0m] in 0 seconds > Running Function12/test.desc [[32mOK[0m] in 0 seconds > Running Function13/test.desc [[32mOK[0m] in 0 seconds > Running Function14/test.desc [[32mOK[0m] in 0 seconds > Running Function2/test.desc [[32mOK[0m] in 0 seconds > Running Function3/test.desc [[32mOK[0m] in 0 seconds > Running Function4/test.desc [[32mOK[0m] in 0 seconds > Running Function5/test.desc [[32mOK[0m] in 0 seconds > Running Function6/test.desc [[32mOK[0m] in 0 seconds > Running Function7/test.desc [[32mOK[0m] in 0 seconds > Running Function8/test.desc [[32mOK[0m] in 0 seconds > Running Function9/test.desc [[32mOK[0m] in 0 seconds > Running Function_Eval_Order1/test.desc [SKIPPED] > Running Function_Eval_Order2/test.desc [[32mOK[0m] in 0 seconds > Running Function_Parameters1/test.desc [SKIPPED] > Running Function_Pointer1/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer10/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer11/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer12/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer13/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer14/test.desc [[32mOK[0m] in 1 seconds > Running Function_Pointer15/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer16/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer17/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer18/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer19/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer2/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer3/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer4/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer5/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer6/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer7/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer8/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer9/test.desc [[32mOK[0m] in 0 seconds > Running Function_Pointer_Init_No_Candidate/test.desc [[32mOK[0m] in 0 > seconds > Running Function_Pointer_Init_One_Candidate/test.desc [[32mOK[0m] in 0 > seconds > Running Function_Pointer_Init_Two_Candidates/test.desc [[32mOK[0m] in 0 > seconds > Running Global_Initialization1/test.desc [[32mOK[0m] in 0 seconds > Running Global_Initialization2/test.desc [[32mOK[0m] in 0 seconds > Running Initialization1/test.desc [[32mOK[0m] in 0 seconds > Running Initialization2/test.desc [[32mOK[0m] in 0 seconds > Running Initialization3/test.desc [[32mOK[0m] in 0 seconds > Running Initialization5/test.desc [[32mOK[0m] in 0 seconds > Running Initialization6/test.desc [[32mOK[0m] in 0 seconds > Running Initialization7/test.desc [[32mOK[0m] in 0 seconds > Running KnR1/test.desc [[32mOK[0m] in 1 seconds > Running Linked_List1/test.desc [[32mOK[0m] in 0 seconds > Running Linking1/test.desc [[32mOK[0m] in 0 seconds > Running Linking2/test.desc [[32mOK[0m] in 0 seconds > Running Linking3/test.desc [[32mOK[0m] in 0 seconds > Running Linking4/test.desc [[32mOK[0m] in 0 seconds > Running Linking5/test.desc [[32mOK[0m] in 0 seconds > Running Linking6/test.desc [[32mOK[0m] in 0 seconds > Running Linking7/member-name-mismatch.desc [[32mOK[0m] in 0 seconds > Running Linking7/return_type.desc [[32mOK[0m] in 0 seconds > Running Linking7/test.desc [[32mOK[0m] in 0 seconds > Running Linking8/test.desc [[32mOK[0m] in 0 seconds > Running Local_out_of_scope1/test.desc [[32mOK[0m] in 0 seconds > Running Local_out_of_scope2/test.desc [[32mOK[0m] in 0 seconds > Running Local_out_of_scope3/test.desc [[32mOK[0m] in 0 seconds > Running Local_out_of_scope4/test.desc [[32mOK[0m] in 0 seconds > Running Malloc1/test.desc [[32mOK[0m] in 0 seconds > Running Malloc10/test.desc [[32mOK[0m] in 1 seconds > Running Malloc11/slice-formula.desc [[32mOK[0m] in 0 seconds > Running Malloc11/test.desc [[32mOK[0m] in 0 seconds > Running Malloc12/test.desc [SKIPPED] > Running Malloc13/test.desc [[32mOK[0m] in 0 seconds > Running Malloc14/test.desc [[32mOK[0m] in 0 seconds > Running Malloc15/test.desc [[32mOK[0m] in 0 seconds > Running Malloc16/test.desc [[32mOK[0m] in 0 seconds > Running Malloc17/test.desc [[32mOK[0m] in 0 seconds > Running Malloc18/test.desc [[32mOK[0m] in 0 seconds > Running Malloc19/test.desc [[32mOK[0m] in 0 seconds > Running Malloc2/test.desc [[32mOK[0m] in 0 seconds > Running Malloc21/test.desc [[32mOK[0m] in 0 seconds > Running Malloc22/test.desc [[32mOK[0m] in 0 seconds > Running Malloc23/test.desc [[32mOK[0m] in 0 seconds > Running Malloc24/test.desc [[32mOK[0m] in 1 seconds > Running Malloc25/test.desc [[32mOK[0m] in 0 seconds > Running Malloc3/test.desc [[32mOK[0m] in 0 seconds > Running Malloc4/test.desc [[32mOK[0m] in 0 seconds > Running Malloc5/test.desc [[32mOK[0m] in 0 seconds > Running Malloc6/test.desc [[32mOK[0m] in 0 seconds > Running Malloc7/test.desc [[32mOK[0m] in 0 seconds > Running Malloc8/test.desc [[32mOK[0m] in 0 seconds > Running Malloc9/test.desc [[32mOK[0m] in 0 seconds > Running Memory_leak1/test.desc [[32mOK[0m] in 0 seconds > Running Memory_leak2/test.desc [[32mOK[0m] in 0 seconds > Running Memory_leak_abort/test.desc [[32mOK[0m] in 1 seconds > Running Minisat_Simp1/test.desc [[32mOK[0m] in 0 seconds > Running Mod1/test.desc [[32mOK[0m] in 0 seconds > Running Mod2/test.desc [[32mOK[0m] in 0 seconds > Running Multi_Dimensional_Array1/test.desc [[32mOK[0m] in 0 seconds > Running Multi_Dimensional_Array2/test.desc [[32mOK[0m] in 0 seconds > Running Multi_Dimensional_Array3/test.desc [[32mOK[0m] in 0 seconds > Running Multi_Dimensional_Array4/test.desc [[32mOK[0m] in 0 seconds > Running Multi_Dimensional_Array5/test.desc [[32mOK[0m] in 0 seconds > Running Multi_Dimensional_Array6/test.desc [[32mOK[0m] in 0 seconds > Running Multiple_Properties1/test.desc [[32mOK[0m] in 0 seconds > Running Negation1/test.desc [[32mOK[0m] in 1 seconds > Running Negation2/test.desc [[32mOK[0m] in 0 seconds > Running Nondet1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer10/test.desc [[32mOK[0m] in 0 seconds > Running Pointer11/test.desc [[32mOK[0m] in 0 seconds > Running Pointer12/test.desc [[32mOK[0m] in 0 seconds > Running Pointer14/test.desc [[32mOK[0m] in 0 seconds > Running Pointer15/test.desc [[32mOK[0m] in 0 seconds > Running Pointer17/test.desc [[32mOK[0m] in 0 seconds > Running Pointer18/full-slice.desc [[32mOK[0m] in 0 seconds > Running Pointer18/test.desc [[32mOK[0m] in 0 seconds > Running Pointer2/test.desc [[32mOK[0m] in 0 seconds > Running Pointer20/test.desc [[32mOK[0m] in 0 seconds > Running Pointer21/test.desc [[32mOK[0m] in 0 seconds > Running Pointer23/test.desc [[32mOK[0m] in 0 seconds > Running Pointer24/test.desc [[32mOK[0m] in 0 seconds > Running Pointer25/test.desc [[32mOK[0m] in 0 seconds > Running Pointer26/test.desc [[32mOK[0m] in 0 seconds > Running Pointer27/test.desc [[32mOK[0m] in 0 seconds > Running Pointer28/test.desc [[32mOK[0m] in 0 seconds > Running Pointer29/test.desc [[32mOK[0m] in 0 seconds > Running Pointer3/test.desc [[32mOK[0m] in 1 seconds > Running Pointer30/test.desc [[32mOK[0m] in 0 seconds > Running Pointer31/test.desc [[32mOK[0m] in 0 seconds > Running Pointer4/test.desc [[32mOK[0m] in 0 seconds > Running Pointer6/test.desc [[32mOK[0m] in 0 seconds > Running Pointer7/test.desc [[32mOK[0m] in 0 seconds > Running Pointer8/test.desc [[32mOK[0m] in 0 seconds > Running Pointer9/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic10/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic11/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic12/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic13/test.desc [SKIPPED] > Running Pointer_Arithmetic14/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic15/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic16/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic17/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic18/test.desc [SKIPPED] > Running Pointer_Arithmetic19/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic2/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic3/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic4/test.desc [[32mOK[0m] in 1 seconds > Running Pointer_Arithmetic5/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic6/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic7/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic8/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Arithmetic9/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Assume1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_Object_Type1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_array1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_array2/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_array3/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_array4/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_array5/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_array6/test.desc [SKIPPED] > Running Pointer_array7/big-endian.desc [[32mOK[0m] in 0 seconds > Running Pointer_array7/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract2/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract3/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract4/program-only.desc [[32mOK[0m] in 1 seconds > Running Pointer_byte_extract4/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract5/no-simplify.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract5/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract6/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract7/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract8/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_byte_extract9/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_comparison1/test.desc [SKIPPED] > Running Pointer_comparison2/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_comparison3/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_comparison4/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_comparison5/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_difference1/no-simplify.desc [[32mOK[0m] in 0 seconds > Running Pointer_difference1/test.desc [[32mOK[0m] in 0 seconds > Running Pointer_difference2/test.desc [[32mOK[0m] in 0 seconds > Running Promotion1/test.desc [[32mOK[0m] in 0 seconds > Running Promotion2/test.desc [[32mOK[0m] in 0 seconds > Running Promotion3/test.desc [[32mOK[0m] in 0 seconds > Running Promotion4/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-assertion/test.desc [[32mOK[0m] in 1 seconds > Running Quantifiers-assignment/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-copy/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-expr-cleaning/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-if/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-initialisation/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-initialisation2/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-invalid-var-range/test.desc [SKIPPED] > Running Quantifiers-not/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-not-exists/fixed.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-simplify/rewrite_exists.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-simplify/rewrite_forall.desc [[32mOK[0m] in 0 seconds > Running Quantifiers-simplify/simplify_not_forall.desc [[32mOK[0m] in 0 > seconds > Running Quantifiers-simplify/test.desc [SKIPPED] > Running Quantifiers-two-dimension-array/fixed.desc [[32mOK[0m] in 0 > seconds > Running Quantifiers-two-dimension-array/test.desc [[32mOK[0m] in 0 > seconds > Running Quantifiers-type/test.desc [SKIPPED] > Running Quantifiers-type2/test.desc [[32mOK[0m] in 0 seconds > Running Quantifiers1/quantifier-with-side-effect.desc [[32mOK[0m] in 0 > seconds > Running Quantifiers1/test.desc [[32mOK[0m] in 0 seconds > Running Recursion1/test.desc [[32mOK[0m] in 0 seconds > Running Recursion2/test.desc [[32mOK[0m] in 0 seconds > Running Recursion3/test.desc [[32mOK[0m] in 0 seconds > Running Recursion4/test.desc [[32mOK[0m] in 1 seconds > Running Recursion5/test.desc [[32mOK[0m] in 0 seconds > Running Recursion6/test.desc [[32mOK[0m] in 0 seconds > Running SIMD1/test.desc [SKIPPED] > Running Same_Basename1/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects1/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects2/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects3/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects4/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects5/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects6/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects7/test.desc [[32mOK[0m] in 0 seconds > Running Sideeffects8/test.desc [[32mOK[0m] in 0 seconds > Running Sizeof1/test.desc [[32mOK[0m] in 0 seconds > Running Static2/test.desc [[32mOK[0m] in 0 seconds > Running Static4/test.desc [[32mOK[0m] in 0 seconds > Running Static_Functions1/test.desc [[32mOK[0m] in 0 seconds > Running String1/test.desc [[32mOK[0m] in 0 seconds > Running String2/test.desc [[32mOK[0m] in 0 seconds > Running String3/test.desc [SKIPPED] > Running String4/test.desc [[32mOK[0m] in 0 seconds > Running String5/test.desc [[32mOK[0m] in 0 seconds > Running String7/test.desc [[32mOK[0m] in 0 seconds > Running String8/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction1/test.desc [[32mOK[0m] in 1 seconds > Running String_Abstraction10/test.desc [SKIPPED] > Running String_Abstraction11/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction12/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction13/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction14/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction15/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction16/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction17/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction18/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction19/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction2/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction20/test.desc [[32mOK[0m] in 1 seconds > Running String_Abstraction21/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction22/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction23/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction24/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction3/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction4/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction5/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction6/test.desc [SKIPPED] > Running String_Abstraction7/test.desc [[31mFAILED[0m] > Running String_Abstraction8/test.desc [[32mOK[0m] in 0 seconds > Running String_Abstraction9/test.desc [[32mOK[0m] in 0 seconds > Running String_Literal1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Array1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Bytewise1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Bytewise2/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization10/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization2/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization3/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization4/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization5/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization6/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization7/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization8/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Initialization9/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Padding1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Pointer1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Pointer2/test.desc [[32mOK[0m] in 1 seconds > Running Struct_Pointer3/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Pointer_Array1/test.desc [[32mOK[0m] in 0 seconds > Running Struct_Propagation1/test.desc [[32mOK[0m] in 0 seconds > Running Type_Error1/test.desc [[32mOK[0m] in 0 seconds > Running Typecast1/test.desc [[32mOK[0m] in 0 seconds > Running Typecast2/test.desc [[32mOK[0m] in 0 seconds > Running Typecast3/test.desc [[32mOK[0m] in 0 seconds > Running Unbounded_Array1/test.desc [[32mOK[0m] in 0 seconds > Running Unbounded_Array2/test.desc [[32mOK[0m] in 0 seconds > Running Unbounded_Array3/test.desc [[32mOK[0m] in 0 seconds > Running Unbounded_Array4/test.desc [[32mOK[0m] in 0 seconds > Running Unbounded_Array5/test.desc [[32mOK[0m] in 0 seconds > Running Unbounded_Array6/test.desc [[32mOK[0m] in 0 seconds > Running Undefined_Function1/test.desc [[32mOK[0m] in 0 seconds > Running Undefined_Function2/test.desc [[32mOK[0m] in 0 seconds > Running Undefined_Shift1/test.desc [[32mOK[0m] in 0 seconds > Running Union_Initialization1/test.desc [[32mOK[0m] in 0 seconds > Running Union_Initialization2/test.desc [[32mOK[0m] in 0 seconds > Running Union_Initialization5/test.desc [[32mOK[0m] in 0 seconds > Running Unwinding_Assertions_Improved1/test.desc [SKIPPED] > Running Unwinding_Locality1/test.desc [[32mOK[0m] in 0 seconds > Running Variadic1/test.desc [[32mOK[0m] in 0 seconds > Running Visual_Studio_Types1/test.desc [[32mOK[0m] in 0 seconds > Running Visual_Studio_Types2/test.desc [[32mOK[0m] in 0 seconds > Running Volatile1/test.desc [SKIPPED] > Running Zero_Initialization1/test.desc [[32mOK[0m] in 1 seconds > Running __builtin_clz-01/big-endian.desc [[32mOK[0m] in 0 seconds > Running __builtin_clz-01/test.desc [[32mOK[0m] in 0 seconds > Running __builtin_ctz-01/big-endian.desc [[32mOK[0m] in 0 seconds > Running __builtin_ctz-01/test.desc [[32mOK[0m] in 0 seconds > Running __builtin_ffs-01/big-endian.desc [[32mOK[0m] in 0 seconds > Running __builtin_ffs-01/test.desc [[32mOK[0m] in 0 seconds > Running __func__1/test.desc [[32mOK[0m] in 0 seconds > Running address_of_struct_member/test.desc [[32mOK[0m] in 0 seconds > Running address_of_struct_member_rec/test.desc [[32mOK[0m] in 0 seconds > Running address_space_size_limit1/test.desc [[32mOK[0m] in 5 seconds > Running address_space_size_limit2/test.desc [SKIPPED] > Running address_space_size_limit3/test.desc [[32mOK[0m] in 10 seconds > Running always_inline1/test.desc [[32mOK[0m] in 0 seconds > Running always_inline2/test.desc [[32mOK[0m] in 0 seconds > Running always_inline3/test.desc [[32mOK[0m] in 0 seconds > Running apply_condition1/test.desc [[32mOK[0m] in 0 seconds > Running argc-and-argv/argc1.desc [[32mOK[0m] in 0 seconds > Running argc-and-argv/argv1.desc [[32mOK[0m] in 0 seconds > Running argv2/test.desc [[32mOK[0m] in 0 seconds > Running array-bug-6230/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity1/test.desc [[32mOK[0m] in 1 seconds > Running array-cell-sensitivity1/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity10/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity10/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity11/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity11/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity12/test.desc [SKIPPED] > Running array-cell-sensitivity12/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity13/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity13/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity14/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity14/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity15/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity2/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity2/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity3/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity3/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity4/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity4/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity5/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity5/test_execution.desc [[32mOK[0m] in 1 > seconds > Running array-cell-sensitivity6/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity6/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity7/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity7/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity8/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity8/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-cell-sensitivity9/test.desc [[32mOK[0m] in 0 seconds > Running array-cell-sensitivity9/test_execution.desc [[32mOK[0m] in 0 > seconds > Running array-constraint/test.desc [[32mOK[0m] in 0 seconds > Running array-constraint/test_json.desc [SKIPPED] > Running array-constraint/test_xml.desc [[32mOK[0m] in 0 seconds > Running array-function-parameters/test.desc [[32mOK[0m] in 0 seconds > Running array-tests/test.desc [[32mOK[0m] in 1 seconds > Running array-tests/uf-always.desc [[32mOK[0m] in 1 seconds > Running array-tests/zero-sized.desc [[32mOK[0m] in 0 seconds > Running array_constraints1/test.desc [[32mOK[0m] in 0 seconds > Running array_of_bool_as_bitvec/test-smt2-outfile.desc [[32mOK[0m] in 0 > seconds > Running assert_func_four/test.desc [[32mOK[0m] in 0 seconds > Running assert_lhs/test.desc [[32mOK[0m] in 0 seconds > Running assert_one/test.desc [[32mOK[0m] in 0 seconds > Running assert_rtn_four/test.desc [[32mOK[0m] in 0 seconds > Running assigning_nullpointers_should_not_crash_symex/test.desc > [[32mOK[0m] in 0 seconds > Running atomic_X_fetch-1/pointer.desc [[32mOK[0m] in 0 seconds > Running atomic_X_fetch-1/test.desc [[32mOK[0m] in 0 seconds > Running atomic_X_fetch-1/two.desc [[32mOK[0m] in 0 seconds > Running atomic_fetch_X-1/pointer.desc [[32mOK[0m] in 0 seconds > Running atomic_fetch_X-1/test.desc [[32mOK[0m] in 0 seconds > Running atomic_fetch_X-1/two.desc [[32mOK[0m] in 0 seconds > Running atomic_load_store-1/test.desc [[32mOK[0m] in 0 seconds > Running atomic_section_seq1/test.desc [[32mOK[0m] in 0 seconds > Running aws-byte-buf-regression/test.desc [[32mOK[0m] in 0 seconds > Running bad_option/test.desc [[32mOK[0m] in 0 seconds > Running bad_option/test_multiple.desc [[32mOK[0m] in 0 seconds > Running big-endian-array1/test.desc [[32mOK[0m] in 1 seconds > Running bounds_check1/test.desc [[32mOK[0m] in 3 seconds > Running bounds_check2/test.desc [[32mOK[0m] in 0 seconds > Running byte-op-metric/test.desc [[32mOK[0m] in 0 seconds > Running byte-op-metric/test_json.desc [[32mOK[0m] in 0 seconds > Running byte_extract1/test.desc [[32mOK[0m] in 0 seconds > Running byte_extract2/test.desc [[32mOK[0m] in 0 seconds > Running byte_update1/test.desc [[32mOK[0m] in 0 seconds > Running byte_update10/test.desc [[32mOK[0m] in 0 seconds > Running byte_update11/test.desc [[32mOK[0m] in 0 seconds > Running byte_update12/test.desc [[32mOK[0m] in 0 seconds > Running byte_update13/test.desc [[32mOK[0m] in 1 seconds > Running byte_update14/test.desc [[32mOK[0m] in 0 seconds > Running byte_update15/test.desc [[32mOK[0m] in 0 seconds > Running byte_update16/big-endian.desc [[32mOK[0m] in 0 seconds > Running byte_update16/little-endian.desc [[32mOK[0m] in 0 seconds > Running byte_update17/test.desc [[32mOK[0m] in 0 seconds > Running byte_update18/test.desc [[32mOK[0m] in 0 seconds > Running byte_update2/test.desc [[32mOK[0m] in 0 seconds > Running byte_update3/test.desc [[32mOK[0m] in 0 seconds > Running byte_update4/test.desc [[32mOK[0m] in 0 seconds > Running byte_update5/full-slice.desc [[32mOK[0m] in 0 seconds > Running byte_update5/test.desc [[32mOK[0m] in 0 seconds > Running byte_update6/test.desc [[32mOK[0m] in 0 seconds > Running byte_update7/test.desc [[32mOK[0m] in 1 seconds > Running byte_update8/test.desc [[32mOK[0m] in 0 seconds > Running byte_update9/test.desc [[32mOK[0m] in 0 seconds > Running c99_Bool/test.desc [[32mOK[0m] in 0 seconds > Running char1/test.desc [[32mOK[0m] in 0 seconds > Running character_handling1/test.desc [[32mOK[0m] in 0 seconds > Running clang_builtins/bitreverse-typeconflict.desc [[32mOK[0m] in 0 > seconds > Running clang_builtins/bitreverse.desc [[32mOK[0m] in 0 seconds > Running clang_builtins/rotate.desc [[32mOK[0m] in 0 seconds > Running comma1/test.desc [[32mOK[0m] in 0 seconds > Running compact-trace/test.desc [[32mOK[0m] in 0 seconds > Running complex1/test.desc [[32mOK[0m] in 0 seconds > Running compound-assignment/compound_promotion.desc [[32mOK[0m] in 0 > seconds > Running compound_literal1/test.desc [[32mOK[0m] in 0 seconds > Running condition-propagation-1/test.desc [[32mOK[0m] in 0 seconds > Running condition-propagation-2/test.desc [[32mOK[0m] in 0 seconds > Running condition-propagation-3/test.desc [[32mOK[0m] in 0 seconds > Running condition-propagation-4/test.desc [[32mOK[0m] in 0 seconds > Running const_ptr1/test.desc [[32mOK[0m] in 0 seconds > Running constant_folding1/test.desc [[32mOK[0m] in 1 seconds > Running constant_folding2/test.desc [[32mOK[0m] in 0 seconds > Running constant_folding3/test.desc [[32mOK[0m] in 0 seconds > Running constructor1/test.desc [[32mOK[0m] in 0 seconds > Running constructor2/test.desc [[32mOK[0m] in 0 seconds > Running cover-failed-assertions/test-no-failed-assertions.desc > [[32mOK[0m] in 0 seconds > Running cover-failed-assertions/test.desc [[32mOK[0m] in 0 seconds > Running coverage_report1/paths.desc [[32mOK[0m] in 0 seconds > Running coverage_report1/test.desc [[32mOK[0m] in 0 seconds > Running coverage_report2/test.desc [[32mOK[0m] in 0 seconds > Running cprover_assert_lhs/test.desc [SKIPPED] > Running cprover_assert_two/test.desc [[32mOK[0m] in 0 seconds > Running cprover_bool1/test.desc [[32mOK[0m] in 0 seconds > Running cprover_fence_one/test.desc [[32mOK[0m] in 0 seconds > Running cprover_havoc_object_lhs/test.desc [SKIPPED] > Running cprover_havoc_object_one/test.desc [[32mOK[0m] in 0 seconds > Running cprover_id1/test.desc [[32mOK[0m] in 0 seconds > Running cprover_input_lhs/test.desc [SKIPPED] > Running cprover_output_lhs/test.desc [SKIPPED] > Running cprover_postcondition/test.desc [[32mOK[0m] in 0 seconds > Running cprover_precondition/test.desc [[32mOK[0m] in 0 seconds > Running dereference-cache-flag/test-no-cache.desc [[32mOK[0m] in 0 > seconds > Running dereference-cache-flag/test-with-cache.desc [[32mOK[0m] in 0 > seconds > Running destructor1/test.desc [[32mOK[0m] in 0 seconds > Running destructors/compound_literal.desc [[32mOK[0m] in 0 seconds > Running destructors/enter_lexical_block.desc [[32mOK[0m] in 0 seconds > Running divide-by-one-simplify/test.desc [[32mOK[0m] in 2 seconds > Running double_deref/double_deref.desc [[32mOK[0m] in 0 seconds > Running double_deref/double_deref_single_alias.desc [[32mOK[0m] in 0 > seconds > Running double_deref/double_deref_with_cast.desc [[32mOK[0m] in 0 seconds > Running double_deref/double_deref_with_cast_single_alias.desc > [[32mOK[0m] in 0 seconds > Running double_deref/double_deref_with_member.desc [[32mOK[0m] in 0 > seconds > Running double_deref/double_deref_with_member_single_alias.desc > [[32mOK[0m] in 1 seconds > Running double_deref/double_deref_with_pointer_arithmetic.desc > [[32mOK[0m] in 0 seconds > Running double_deref/double_deref_with_pointer_arithmetic_single_alias.desc > [[32mOK[0m] in 0 seconds > Running dynamic_size1/stack_object.desc [[32mOK[0m] in 0 seconds > Running dynamic_size1/test.desc [[32mOK[0m] in 0 seconds > Running dynamic_sizeof1/test.desc [[32mOK[0m] in 0 seconds > Running empty_compound_type1/test.desc [[32mOK[0m] in 0 seconds > Running empty_compound_type2/test.desc [[32mOK[0m] in 0 seconds > Running empty_compound_type3/test.desc [[32mOK[0m] in 0 seconds > Running empty_compound_type4/test.desc [[32mOK[0m] in 0 seconds > Running enum-trace1/test_json.desc [[32mOK[0m] in 0 seconds > Running enum-trace1/test_xml.desc [[32mOK[0m] in 0 seconds > Running enum1/test.desc [[32mOK[0m] in 0 seconds > Running enum2/test.desc [[32mOK[0m] in 0 seconds > Running enum3/test.desc [[32mOK[0m] in 0 seconds > Running enum4/test.desc [[32mOK[0m] in 0 seconds > Running enum5/test.desc [[32mOK[0m] in 0 seconds > Running enum6/test.desc [[32mOK[0m] in 0 seconds > Running enum7/test.desc [[32mOK[0m] in 0 seconds > Running enum8/test.desc [[32mOK[0m] in 1 seconds > Running enum9/test.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/enum_test3-simplified.desc [[32mOK[0m] in 0 > seconds > Running enum_is_in_range/enum_test3.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/enum_test4.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/enum_test5.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/enum_test7.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/enum_test8.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/format.desc [[32mOK[0m] in 0 seconds > Running enum_is_in_range/no_duplicate.desc [[32mOK[0m] in 0 seconds > Running enum_underlying_type_01/test.desc [[32mOK[0m] in 0 seconds > Running enum_underlying_type_02/test.desc [[32mOK[0m] in 0 seconds > Running enum_underlying_type_03/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array1/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array2/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array3/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array4/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array5/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array6/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_array_of_struct1/test.desc [[32mOK[0m] in 0 > seconds > Running equality_through_array_of_struct2/test.desc [[32mOK[0m] in 0 > seconds > Running equality_through_array_of_struct3/test.desc [[32mOK[0m] in 0 > seconds > Running equality_through_array_of_struct4/test.desc [[32mOK[0m] in 1 > seconds > Running equality_through_struct1/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_struct2/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_struct3/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_struct4/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_struct_containing_arrays1/test.desc [[32mOK[0m] > in 0 seconds > Running equality_through_struct_containing_arrays2/test.desc [[32mOK[0m] > in 0 seconds > Running equality_through_union1/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_union2/test.desc [[32mOK[0m] in 0 seconds > Running equality_through_union3/test.desc [[32mOK[0m] in 0 seconds > Running exit1/test.desc [[32mOK[0m] in 0 seconds > Running export-symex-ready-goto/test-bad-usage.desc [[32mOK[0m] in 0 > seconds > Running export-symex-ready-goto/test-correct.desc [[32mOK[0m] in 0 > seconds > Running extern1/test.desc [[32mOK[0m] in 0 seconds > Running extern2/test.desc [[32mOK[0m] in 0 seconds > Running extern3/test.desc [[32mOK[0m] in 0 seconds > Running extern4/test.desc [[32mOK[0m] in 0 seconds > Running extern5/test.desc [[32mOK[0m] in 0 seconds > Running extern_initialization1/test.desc [[32mOK[0m] in 0 seconds > Running extern_initialization2/test.desc [[32mOK[0m] in 0 seconds > Running fault_localization-all_properties1/test.desc [SKIPPED] > Running fault_localization-all_properties2/test.desc [SKIPPED] > Running fault_localization-stop_on_fail1/test.desc [[32mOK[0m] in 0 > seconds > Running field-sensitivity-trace-wrong-counterexample-1/test.desc > [[32mOK[0m] in 0 seconds > Running field-sensitivity1/test.desc [[32mOK[0m] in 1 seconds > Running field-sensitivity10/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity11/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity12/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity13/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity14/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity15/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity16/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity2/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity3/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity4/test.desc [SKIPPED] > Running field-sensitivity5/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity6/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity7/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity8/test.desc [[32mOK[0m] in 0 seconds > Running field-sensitivity9/test.desc [[32mOK[0m] in 0 seconds > Running float-nan-check/test.desc [[32mOK[0m] in 1 seconds > Running fmod1/test.desc [[32mOK[0m] in 0 seconds > Running for-break1/test.desc [[32mOK[0m] in 0 seconds > Running for1/test.desc [[32mOK[0m] in 0 seconds > Running for2/test.desc [[32mOK[0m] in 0 seconds > Running for3/test.desc [[32mOK[0m] in 0 seconds > Running full_slice1/test.desc [[32mOK[0m] in 0 seconds > Running full_slice2/test.desc [[32mOK[0m] in 0 seconds > Running full_slice3/test.desc [[32mOK[0m] in 0 seconds > Running function-return-no-body1/test.desc [[32mOK[0m] in 0 seconds > Running function_not_found/test.desc [SKIPPED] > Running function_option1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_attribute_alias1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_bswap1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_builtin_add_overflow/test.desc [[32mOK[0m] in 0 seconds > Running gcc_builtin_add_overflow/type-conflict-2.desc [[32mOK[0m] in 0 > seconds > Running gcc_builtin_add_overflow/type-conflict.desc [[32mOK[0m] in 0 > seconds > Running gcc_builtin_mul_overflow/test.desc [[32mOK[0m] in 1 seconds > Running gcc_builtin_sub_overflow/simplify.desc [[32mOK[0m] in 0 seconds > Running gcc_builtin_sub_overflow/test.desc [[32mOK[0m] in 0 seconds > Running gcc_builtin_va_arg_one/test.desc [[32mOK[0m] in 0 seconds > Running gcc_c99-bool-1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_conditional_expr1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_local_label1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_popcount1/test.desc [[32mOK[0m] in 1 seconds > Running gcc_popcount2/test.desc [SKIPPED] > Running gcc_statement_expression1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_statement_expression2/test.desc [[32mOK[0m] in 1 seconds > Running gcc_statement_expression3/test.desc [[32mOK[0m] in 0 seconds > Running gcc_statement_expression4/test.desc [[32mOK[0m] in 0 seconds > Running gcc_statement_expression5/test.desc [[32mOK[0m] in 0 seconds > Running gcc_switch_case_range1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_switch_case_range2/test.desc [[32mOK[0m] in 0 seconds > Running gcc_vector1/test.desc [[32mOK[0m] in 0 seconds > Running gcc_vector2/test.desc [[32mOK[0m] in 0 seconds > Running gcc_vector3/test.desc [[32mOK[0m] in 0 seconds > Running goto1/test.desc [[32mOK[0m] in 0 seconds > Running goto2/test.desc [[32mOK[0m] in 0 seconds > Running goto3/test.desc [[32mOK[0m] in 0 seconds > Running goto4/test.desc [[32mOK[0m] in 0 seconds > Running goto5/test.desc [[32mOK[0m] in 0 seconds > Running graphml_witness1/test.desc [[32mOK[0m] in 0 seconds > Running graphml_witness2/test.desc [[32mOK[0m] in 0 seconds > Running guard1/test.desc [[32mOK[0m] in 0 seconds > Running havoc_choice/test.desc [[32mOK[0m] in 0 seconds > Running havoc_object1/full-slice.desc [[32mOK[0m] in 0 seconds > Running havoc_object1/test.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_array_slice_1.desc [[32mOK[0m] in 1 seconds > Running havoc_slice/test_array_slice_2.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_array_symbolic_size.desc [[32mOK[0m] in 0 > seconds > Running havoc_slice/test_nondet_conditional.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_a.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_b.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_b_slice.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_c.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_d.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_raw_bytes.desc [SKIPPED] > Running havoc_slice/test_struct_union_a.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_union_b.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_union_b_slice.desc [[32mOK[0m] in 0 > seconds > Running havoc_slice/test_struct_union_c.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_struct_union_d.desc [[32mOK[0m] in 0 seconds > Running havoc_slice/test_whole_array.desc [[32mOK[0m] in 1 seconds > Running havoc_slice/test_whole_array_with_offset.desc [[32mOK[0m] in 0 > seconds > Running havoc_slice_checks/full-slice.desc [[32mOK[0m] in 0 seconds > Running havoc_slice_checks/test.desc [[32mOK[0m] in 0 seconds > Running havoc_undefined_functions/test.desc [[32mOK[0m] in 0 seconds > Running hex_string1/test.desc [[32mOK[0m] in 0 seconds > Running hex_trace/test.desc [[32mOK[0m] in 0 seconds > Running if1/test.desc [[32mOK[0m] in 0 seconds > Running if2/test.desc [[32mOK[0m] in 0 seconds > Running if3/test.desc [[32mOK[0m] in 0 seconds > Running if4/test.desc [[32mOK[0m] in 0 seconds > Running incomplete-sizeof/array.desc [[32mOK[0m] in 0 seconds > Running incomplete-sizeof/enum.desc [[32mOK[0m] in 0 seconds > Running incomplete-sizeof/struct.desc [[32mOK[0m] in 0 seconds > Running incomplete-sizeof/union.desc [[32mOK[0m] in 0 seconds > Running incomplete-structs/test.desc [[32mOK[0m] in 0 seconds > Running inequality-with-constant-normalisation/test.desc [[32mOK[0m] in > 0 seconds > Running inequality-with-constant-normalisation1/test.desc [[32mOK[0m] in > 0 seconds > Running inline1/test.desc [[32mOK[0m] in 1 seconds > Running integer-assignments1/integer-typecheck.desc [[32mOK[0m] in 0 > seconds > Running integer-assignments1/test.desc [SKIPPED] > Running integer-pointer/test.desc [SKIPPED] > Running integral-trace/test.desc [[32mOK[0m] in 0 seconds > Running issue_5952_soundness_bug_smt_encoding/test_original.desc [SKIPPED] > Running issue_5952_soundness_bug_smt_encoding/test_short.desc [SKIPPED] > Running json-interface1/test.desc [[32mOK[0m] in 0 seconds > Running json-interface1/test_wrong_flag.desc [[32mOK[0m] in 0 seconds > Running json-interface1/test_wrong_option.desc [[32mOK[0m] in 0 seconds > Running json-ui/no_entry.desc [[32mOK[0m] in 0 seconds > Running json-ui/syntax_error.desc [[32mOK[0m] in 0 seconds > Running json1/test.desc [[32mOK[0m] in 0 seconds > Running lhs-pointer-aliases-constant/test.desc [[32mOK[0m] in 0 seconds > Running link_json_symtabs/test.desc [[32mOK[0m] in 0 seconds > Running little-endian-array1/test.desc [[32mOK[0m] in 0 seconds > Running locations1/test.desc [[32mOK[0m] in 0 seconds > Running loophead-trace/test-json.desc [[32mOK[0m] in 0 seconds > Running loophead-trace/test-xml.desc [[32mOK[0m] in 0 seconds > Running malloc-may-fail/test.desc [[32mOK[0m] in 0 seconds > Running malloc-may-fail/test_without_option.desc [[32mOK[0m] in 0 seconds > Running malloc-too-large/largest_representable.desc [[32mOK[0m] in 0 > seconds > Running malloc-too-large/max_size.desc [[32mOK[0m] in 1 seconds > Running malloc-too-large/one_byte_too_large.desc [[32mOK[0m] in 0 seconds > Running member1/test.desc [[32mOK[0m] in 0 seconds > Running member_bounds3/test.desc [SKIPPED] > Running member_bounds4/test.desc [SKIPPED] > Running memory_allocation1/test.desc [[32mOK[0m] in 0 seconds > Running memory_allocation2/test.desc [[32mOK[0m] in 0 seconds > Running memset1/test.desc [[32mOK[0m] in 0 seconds > Running memset2/test.desc [[32mOK[0m] in 0 seconds > Running memset3/test.desc [[32mOK[0m] in 0 seconds > Running memset_null/test.desc [[32mOK[0m] in 0 seconds > Running mm_io1/test.desc [[32mOK[0m] in 0 seconds > Running multiple-goto-traces/test.desc [[32mOK[0m] in 0 seconds > Running nested_label1/test.desc [[32mOK[0m] in 0 seconds > Running no-propagation/test.desc [[32mOK[0m] in 0 seconds > Running no_nondet_static/test.desc [[32mOK[0m] in 0 seconds > Running nondet-pointer/nondet-pointer1.desc [[32mOK[0m] in 0 seconds > Running nondet-pointer/nondet-pointer2.desc [[32mOK[0m] in 0 seconds > Running nondet-pointer/nondet-pointer3.desc [[32mOK[0m] in 1 seconds > Running nondet-pointer/nondet-pointer4.desc [[32mOK[0m] in 0 seconds > Running nondet-pointer/nondet-pointer5.desc [[32mOK[0m] in 0 seconds > Running noop1/test.desc [[32mOK[0m] in 0 seconds > Running noop2/test.desc [[32mOK[0m] in 0 seconds > Running null1/test.desc [[32mOK[0m] in 0 seconds > Running null2/test.desc [[32mOK[0m] in 0 seconds > Running null3/test.desc [[32mOK[0m] in 0 seconds > Running null4/test.desc [[32mOK[0m] in 0 seconds > Running null5/test.desc [[32mOK[0m] in 0 seconds > Running null6/test.desc [[32mOK[0m] in 0 seconds > Running null7/test.desc [[32mOK[0m] in 0 seconds > Running null8/test.desc [[32mOK[0m] in 0 seconds > Running object-bits-parsing/non_numeric.desc [[32mOK[0m] in 0 seconds > Running object-bits-parsing/too_large.desc [[32mOK[0m] in 0 seconds > Running object-bits-parsing/valid.desc [[32mOK[0m] in 0 seconds > Running object-bits-parsing/zero.desc [[32mOK[0m] in 0 seconds > Running offsetof1/test.desc [[32mOK[0m] in 0 seconds > Running overflow/leftshift_overflow-c89.desc [[32mOK[0m] in 0 seconds > Running overflow/leftshift_overflow-c99-full-slice.desc [[32mOK[0m] in 0 > seconds > Running overflow/leftshift_overflow-c99.desc [[32mOK[0m] in 0 seconds > Running overflow/mod_overflow.desc [[32mOK[0m] in 0 seconds > Running overflow/signed_addition_overflow1.desc [[32mOK[0m] in 0 seconds > Running overflow/signed_addition_overflow2.desc [[32mOK[0m] in 0 seconds > Running overflow/signed_addition_overflow3.desc [[32mOK[0m] in 0 seconds > Running overflow/signed_addition_overflow4.desc [[32mOK[0m] in 1 seconds > Running overflow/signed_multiplication1.desc [[32mOK[0m] in 0 seconds > Running overflow/signed_subtraction1.desc [[32mOK[0m] in 0 seconds > Running overflow/unary_minus_overflow.desc [[32mOK[0m] in 0 seconds > Running path-branch-pointer-call/test.desc [[32mOK[0m] in 0 seconds > Running path-per-path-vccs/test.desc [[32mOK[0m] in 0 seconds > Running phi-merge_uninitialized_values/dynamic.desc [[32mOK[0m] in 0 > seconds > Running phi-merge_uninitialized_values/global.desc [[32mOK[0m] in 0 > seconds > Running phi-merge_uninitialized_values/local.desc [[32mOK[0m] in 0 > seconds > Running phi-merge_uninitialized_values/static_local.desc [[32mOK[0m] in > 0 seconds > Running pointer-check-01/test.desc [[32mOK[0m] in 0 seconds > Running pointer-check-02/test.desc [[32mOK[0m] in 0 seconds > Running pointer-extra-checks/test.desc [[32mOK[0m] in 0 seconds > Running pointer-function-parameters/test.desc [[32mOK[0m] in 0 seconds > Running pointer-function-parameters-struct-mutual-recursion/test.desc > [[32mOK[0m] in 0 seconds > Running pointer-function-parameters-struct-non-recursive/test.desc > [[32mOK[0m] in 0 seconds > Running pointer-function-parameters-struct-simple-recursion/test.desc > [[32mOK[0m] in 0 seconds > Running pointer-function-parameters-struct-simple-recursion-2/test.desc > [[32mOK[0m] in 1 seconds > Running pointer-offset-01/test.desc [[32mOK[0m] in 0 seconds > Running pointer-overflow1/test.desc [[32mOK[0m] in 0 seconds > Running pointer-overflow2/test.desc [[32mOK[0m] in 0 seconds > Running pointer-overflow3/no-simplify.desc [[32mOK[0m] in 0 seconds > Running pointer-overflow3/test.desc [[32mOK[0m] in 0 seconds > Running pointer-overflow4/test.desc [[32mOK[0m] in 0 seconds > Running pointer-predicates/at_bounds1.desc [[32mOK[0m] in 0 seconds > Running pointer-predicates/in_range1.desc [[32mOK[0m] in 0 seconds > Running pointer-primitive-check-01/test.desc [[32mOK[0m] in 0 seconds > Running pointer-primitive-check-02/test.desc [[32mOK[0m] in 0 seconds > Running pointer-primitive-check-04/test.desc [[32mOK[0m] in 0 seconds > Running > pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc > [[32mOK[0m] in 0 seconds > Running points-to-sets/test.desc [[32mOK[0m] in 0 seconds > Running points-to-sets/test_json.desc [[32mOK[0m] in 0 seconds > Running points-to-sets/test_xml.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover1/test.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover2/test.desc [[32mOK[0m] in 1 seconds > Running pragma_cprover3/test.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover_enable1/test.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover_enable2/test.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover_enable3/test.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover_enable_all/test.desc [[32mOK[0m] in 0 seconds > Running pragma_cprover_enable_disable_global_off/test.desc [[32mOK[0m] > in 0 seconds > Running pragma_cprover_enable_disable_global_on/test.desc [[32mOK[0m] in > 0 seconds > Running pragma_cprover_enable_disable_multiple/test.desc [[32mOK[0m] in > 0 seconds > Running printf1/test.desc [[32mOK[0m] in 0 seconds > Running ptr_arithmetic_on_null/test.desc [[32mOK[0m] in 0 seconds > Running ptr_arithmetic_on_null/type_conflict.desc [[32mOK[0m] in 0 > seconds > Running r_w_ok1/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok10/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok2/test.desc [[32mOK[0m] in 1 seconds > Running r_w_ok3/test.desc [SKIPPED] > Running r_w_ok4/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok5/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok6/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok7/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok8/test.desc [[32mOK[0m] in 0 seconds > Running r_w_ok9/simplify.desc [[32mOK[0m] in 0 seconds > Running r_w_ok9/test.desc [[32mOK[0m] in 0 seconds > Running reachability-slice/test.desc [[32mOK[0m] in 0 seconds > Running reachability-slice/test2.desc [[32mOK[0m] in 0 seconds > Running reachability-slice/test3.desc [[32mOK[0m] in 0 seconds > Running reachability-slice-interproc/test.desc [[32mOK[0m] in 0 seconds > Running reachability-slice-interproc2/test.desc [[32mOK[0m] in 0 seconds > Running reachability-slice-interproc3/test.desc [[32mOK[0m] in 0 seconds > Running realloc-should-not-free-on-failure-to-allocate/test.desc > [[32mOK[0m] in 0 seconds > Running residual-guards-1/test.desc [[32mOK[0m] in 0 seconds > Running residual-guards-1/test_execution.desc [[32mOK[0m] in 0 seconds > Running residual-guards-2/test.desc [[32mOK[0m] in 1 seconds > Running residual-guards-2/test_execution.desc [[32mOK[0m] in 0 seconds > Running residual-guards-2/unreachable-code.desc [SKIPPED] > Running residual-guards-3/test.desc [[32mOK[0m] in 0 seconds > Running residual-guards-3/test_execution.desc [[32mOK[0m] in 0 seconds > Running residual-guards-4/test.desc [[32mOK[0m] in 0 seconds > Running residual-guards-4/test_execution.desc [[32mOK[0m] in 0 seconds > Running residual-guards-4/unreachable-code.desc [SKIPPED] > Running return1/test.desc [[32mOK[0m] in 0 seconds > Running return2/test.desc [[32mOK[0m] in 0 seconds > Running return3/full-slice.desc [[32mOK[0m] in 0 seconds > Running return3/test.desc [[32mOK[0m] in 0 seconds > Running return4/test.desc [[32mOK[0m] in 0 seconds > Running return5/test.desc [[32mOK[0m] in 0 seconds > Running return6/test.desc [[32mOK[0m] in 0 seconds > Running return7/test.desc [[32mOK[0m] in 0 seconds > Running return8/test.desc [[32mOK[0m] in 0 seconds > Running return9/test.desc [[32mOK[0m] in 0 seconds > Running runtime-profiling/test.desc [[32mOK[0m] in 0 seconds > Running sat-solver/test.desc [[32mOK[0m] in 1 seconds > Running sat-solver-error/test.desc [[32mOK[0m] in 0 seconds > Running sat-solver-warning/test.desc [[32mOK[0m] in 0 seconds > Running saturating_arithmetric/output-formula.desc [[32mOK[0m] in 0 > seconds > Running saturating_arithmetric/output-goto.desc [[32mOK[0m] in 0 seconds > Running saturating_arithmetric/test.desc [[32mOK[0m] in 0 seconds > Running saturating_arithmetric/typeconflict.desc [[32mOK[0m] in 0 seconds > Running scanf1/big-endian.desc [[32mOK[0m] in 0 seconds > Running scanf1/no-simplify.desc [SKIPPED] > Running scanf1/test.desc [[32mOK[0m] in 0 seconds > Running self_loops_to_assumptions1/default.desc [[32mOK[0m] in 0 seconds > Running self_loops_to_assumptions1/no-assume.desc [[32mOK[0m] in 0 > seconds > Running set-property-inline1/test.desc [[32mOK[0m] in 0 seconds > Running short_circuit_implies/false_implies_failure_side_effect.desc > [[32mOK[0m] in 0 seconds > Running short_circuit_implies/short-circuit-memory-checks.desc > [[32mOK[0m] in 0 seconds > Running short_circuit_implies/true_implies_failure_side_effect.desc > [[32mOK[0m] in 0 seconds > Running show-vcc/main_prec.desc [[32mOK[0m] in 0 seconds > Running show-vcc/test.desc [[32mOK[0m] in 0 seconds > Running show_properties1/test.desc [[32mOK[0m] in 0 seconds > Running simplify-array-size/test.desc [[32mOK[0m] in 0 seconds > Running simplify-full-test/test.desc [[32mOK[0m] in 0 seconds > Running simplify-function-call-array-element-pointer/test.desc > [[32mOK[0m] in 0 seconds > Running simplify-function-call-array-pointer/test.desc [[32mOK[0m] in 0 > seconds > Running simplify-function-call-pointer-access/test.desc [[32mOK[0m] in 0 > seconds > Running simplify-global-array-access/test.desc [[32mOK[0m] in 1 seconds > Running simplify-local-array-access/test.desc [[32mOK[0m] in 0 seconds > Running simplify-pointer-access/test.desc [[32mOK[0m] in 0 seconds > Running simplify-union/test.desc [[32mOK[0m] in 0 seconds > Running simplify_singleton_interval_7690/negative_test.desc [[32mOK[0m] > in 0 seconds > Running simplify_singleton_interval_7690/positive_test.desc [[32mOK[0m] > in 0 seconds > Running simplify_singleton_interval_7690/test_smt2.desc [SKIPPED] > Running simplify_singleton_interval_7953/test.desc [[32mOK[0m] in 0 > seconds > Running stack-trace/test.desc [[32mOK[0m] in 0 seconds > Running string_assignment1/test.desc [[32mOK[0m] in 0 seconds > Running struct1/test.desc [[32mOK[0m] in 0 seconds > Running struct10/test.desc [[32mOK[0m] in 0 seconds > Running struct11/test.desc [[32mOK[0m] in 0 seconds > Running struct12/test.desc [[32mOK[0m] in 0 seconds > Running struct13/test.desc [[32mOK[0m] in 0 seconds > Running struct14/test.desc [[32mOK[0m] in 0 seconds > Running struct15/test.desc [SKIPPED] > Running struct16/test.desc [[32mOK[0m] in 0 seconds > Running struct17/test.desc [[32mOK[0m] in 0 seconds > Running struct3/test.desc [[32mOK[0m] in 0 seconds > Running struct4/test.desc [[32mOK[0m] in 0 seconds > Running struct6/test.desc [[32mOK[0m] in 0 seconds > Running struct7/test.desc [[32mOK[0m] in 1 seconds > Running struct8/test.desc [[32mOK[0m] in 0 seconds > Running struct9/test.desc [[32mOK[0m] in 0 seconds > Running switch1/test.desc [[32mOK[0m] in 0 seconds > Running switch2/test.desc [[32mOK[0m] in 0 seconds > Running switch3/test.desc [[32mOK[0m] in 0 seconds > Running switch4/test.desc [[32mOK[0m] in 0 seconds > Running switch5/test.desc [[32mOK[0m] in 0 seconds > Running switch6/test.desc [[32mOK[0m] in 0 seconds > Running switch7/test.desc [[32mOK[0m] in 0 seconds > Running switch8/program-only.desc [[32mOK[0m] in 0 seconds > Running switch8/test.desc [[32mOK[0m] in 0 seconds > Running switch9/test.desc [[32mOK[0m] in 0 seconds > Running symex_should_evaluate_simple_pointer_conditions/test.desc > [[32mOK[0m] in 0 seconds > Running symex_should_exclude_null_pointers/nondet.desc [[32mOK[0m] in 0 > seconds > Running symex_should_exclude_null_pointers/test.desc [[32mOK[0m] in 0 > seconds > Running symex_should_filter_value_sets/test.desc [[32mOK[0m] in 0 seconds > Running sync_X_and_fetch-1/pointer.desc [[32mOK[0m] in 0 seconds > Running sync_X_and_fetch-1/test.desc [[32mOK[0m] in 0 seconds > Running sync_X_and_fetch-1/two.desc [[32mOK[0m] in 0 seconds > Running sync_bool_compare-1/pointer.desc [[32mOK[0m] in 0 seconds > Running sync_bool_compare-1/test.desc [[32mOK[0m] in 1 seconds > Running sync_bool_compare-1/three.desc [[32mOK[0m] in 0 seconds > Running sync_fetch_and_X-1/pointer.desc [[32mOK[0m] in 0 seconds > Running sync_fetch_and_X-1/test.desc [[32mOK[0m] in 0 seconds > Running sync_fetch_and_X-1/two.desc [[32mOK[0m] in 0 seconds > Running sync_lock_release-1/symbol_per_type.desc [[32mOK[0m] in 0 seconds > Running sync_lock_release-1/test.desc [[32mOK[0m] in 0 seconds > Running sync_val_compare-1/pointer.desc [[32mOK[0m] in 0 seconds > Running sync_val_compare-1/test.desc [[32mOK[0m] in 0 seconds > Running sync_val_compare-1/three.desc [[32mOK[0m] in 0 seconds > Running trace-strings/test.desc [[32mOK[0m] in 0 seconds > Running trace-values/trace-values.desc [[32mOK[0m] in 0 seconds > Running trace-values/unbounded_array.desc [[32mOK[0m] in 0 seconds > Running trace_address_arithmetic1/test.desc [[32mOK[0m] in 0 seconds > Running trace_options_json_extended/extended.desc [[32mOK[0m] in 0 > seconds > Running trace_options_json_extended/non-extended.desc [[32mOK[0m] in 0 > seconds > Running trace_show_code/test.desc [[32mOK[0m] in 0 seconds > Running trace_show_function_calls/test.desc [SKIPPED] > Running ts18661_typedefs/test.desc [[32mOK[0m] in 0 seconds > Running typedef-anon-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-anon-struct2/test.desc [[32mOK[0m] in 0 seconds > Running typedef-anon-union1/test.desc [[32mOK[0m] in 1 seconds > Running typedef-anon-union2/test.desc [[32mOK[0m] in 0 seconds > Running typedef-const-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-const-type1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-const-union1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-anon-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-anon-union1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-type1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-type2/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-type3/test.desc [[32mOK[0m] in 0 seconds > Running typedef-param-union1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-anon-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-anon-union1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-type1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-type2/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-type3/test.desc [[32mOK[0m] in 0 seconds > Running typedef-return-union1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-struct1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-struct2/test.desc [[32mOK[0m] in 0 seconds > Running typedef-type1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-type2/test.desc [[32mOK[0m] in 0 seconds > Running typedef-type3/test.desc [[32mOK[0m] in 0 seconds > Running typedef-type4/test.desc [[32mOK[0m] in 0 seconds > Running typedef-union1/test.desc [[32mOK[0m] in 0 seconds > Running typedef-union2/test.desc [[32mOK[0m] in 0 seconds > Running uncaught_exceptions_analysis1/test.desc [[32mOK[0m] in 1 seconds > Running uniform_array1/test.desc [[32mOK[0m] in 0 seconds > Running uninterpreted_function/uf1.desc [[32mOK[0m] in 0 seconds > Running uninterpreted_function/uf2.desc [[32mOK[0m] in 0 seconds > Running union/union_initialization.desc [[32mOK[0m] in 0 seconds > Running union/union_large_array.desc [[32mOK[0m] in 0 seconds > Running union/union_member.desc [[32mOK[0m] in 0 seconds > Running union/union_update.desc [[32mOK[0m] in 0 seconds > Running union-unequal-element-size1/test.desc [[32mOK[0m] in 0 seconds > Running union1/test.desc [[32mOK[0m] in 0 seconds > Running union10/union_list2.desc [[32mOK[0m] in 1 seconds > Running union11/union_list.desc [[32mOK[0m] in 0 seconds > Running union12/test.desc [[32mOK[0m] in 0 seconds > Running union13/no-arch.desc [[32mOK[0m] in 0 seconds > Running union13/test.desc [[32mOK[0m] in 0 seconds > Running union14/test.desc [[32mOK[0m] in 0 seconds > Running union15/test.desc [[32mOK[0m] in 0 seconds > Running union16/test.desc [[32mOK[0m] in 0 seconds > Running union17/test.desc [[32mOK[0m] in 0 seconds > Running union18/test.desc [[32mOK[0m] in 0 seconds > Running union2/test.desc [[32mOK[0m] in 0 seconds > Running union3/test.desc [[32mOK[0m] in 0 seconds > Running union4/test.desc [[32mOK[0m] in 0 seconds > Running union5/test.desc [[32mOK[0m] in 0 seconds > Running union6/test.desc [[32mOK[0m] in 0 seconds > Running union7/test.desc [[32mOK[0m] in 0 seconds > Running union8/test.desc [[32mOK[0m] in 0 seconds > Running union9/test.desc [[32mOK[0m] in 0 seconds > Running unknown-argument-suggestion/test.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto1/test-vccs.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto1/test.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto2/test-vccs.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto2/test.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto3/test-vccs.desc [[32mOK[0m] in 1 seconds > Running unreachable-goto3/test.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto4/test-vccs.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto4/test.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto5/test-vccs.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto5/test.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto6/test-vccs.desc [[32mOK[0m] in 0 seconds > Running unreachable-goto6/test.desc [[32mOK[0m] in 0 seconds > Running unsigned1/test.desc [[32mOK[0m] in 0 seconds > Running unsigned___int128/test.desc [[32mOK[0m] in 0 seconds > Running unsigned_char1/test.desc [[32mOK[0m] in 0 seconds > Running unwind_counters1/test.desc [[32mOK[0m] in 0 seconds > Running unwind_counters2/test.desc [[32mOK[0m] in 0 seconds > Running unwind_counters3/test.desc [[32mOK[0m] in 0 seconds > Running unwind_counters4/test.desc [[32mOK[0m] in 0 seconds > Running unwinding_assertions1/test.desc [[32mOK[0m] in 0 seconds > Running unwindset1/label.desc [[32mOK[0m] in 0 seconds > Running unwindset1/test.desc [[32mOK[0m] in 0 seconds > Running unwindset2/test.desc [[32mOK[0m] in 0 seconds > Running va_list1/test.desc [[32mOK[0m] in 0 seconds > Running va_list2/test.desc [[32mOK[0m] in 0 seconds > Running va_list3/test.desc [[32mOK[0m] in 0 seconds > Running va_list3/windows-preprocessed.desc [[32mOK[0m] in 1 seconds > Running va_list4/test.desc [[32mOK[0m] in 0 seconds > Running variable-access-to-constant-array/test.desc [[32mOK[0m] in 0 > seconds > Running verifier_assume_lhs/test.desc [SKIPPED] > Running verifier_assume_one/test.desc [[32mOK[0m] in 0 seconds > Running verifier_error_lhs/test.desc [[32mOK[0m] in 0 seconds > Running verifier_error_zero/test.desc [[32mOK[0m] in 0 seconds > Running vla1/program-only.desc [[32mOK[0m] in 0 seconds > Running vla1/test.desc [[32mOK[0m] in 0 seconds > Running vla2/test.desc [SKIPPED] > Running vla3/test.desc [SKIPPED] > Running void_ifthenelse/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer1/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer2/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer3/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer4/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer5/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer6/test.desc [[32mOK[0m] in 0 seconds > Running void_pointer7/test.desc [[32mOK[0m] in 0 seconds > Running while1/test.desc [[32mOK[0m] in 0 seconds > Running while2/requires-transform.desc [[32mOK[0m] in 0 seconds > Running while2/test.desc [[32mOK[0m] in 0 seconds > Running xml-escaping/debug_output.desc [[32mOK[0m] in 0 seconds > Running xml-interface1/test.desc [[32mOK[0m] in 0 seconds > Running xml-interface1/test_wrong_flag.desc [[32mOK[0m] in 0 seconds > Running xml-interface1/test_wrong_option.desc [[32mOK[0m] in 0 seconds > Running xml-trace/test.desc [[32mOK[0m] in 0 seconds > Running xml-trace2/test.desc [[32mOK[0m] in 1 seconds > Running z3/invalid.desc [SKIPPED] > Running z3/Issue5970.desc [SKIPPED] > Running z3/Issue5977.desc [SKIPPED] > Running z3/trace-char.desc [SKIPPED] > Running z3/trace.desc [SKIPPED] > Running z3/valid.desc [SKIPPED] > > [31mTests failed[0m > 1 of 1114 tests failed, 60 tests skipped > > > Failed test: String_Abstraction7 > CBMC version 5.95.1 (cbmc-5.95.1) 32-bit armhf linux > Parsing main.c > Converting > Type-checking main > Generating GOTO Program > Adding CPROVER library (armhf) > Removal of function pointers and virtual functions > Generic Property Instrumentation > String Abstraction > Running with 8 object bits, 24 offset bits (default) > Starting Bounded Model Checking > **** WARNING: no body for function fopen64 > Runtime Symex: 0.034871s > size of program expression: 701 steps > simple slicing removed 91 assignments > Generated 14 VCC(s), 10 remaining after simplification > Runtime Postprocess Equation: 0.00141007s > Passing problem to propositional reduction > converting SSA > Runtime Convert SSA: 0.00755571s > Running propositional reduction > Post-processing > Runtime Post-process: 0.00734062s > Solving with MiniSAT 2.2.1 with simplifier > 19821 variables, 9460 clauses > SAT checker: instance is SATISFIABLE > Runtime Solver: 0.0566029s > Runtime decision procedure: 0.0642756s > Running propositional reduction > Solving with MiniSAT 2.2.1 with simplifier > 19821 variables, 2826 clauses > SAT checker: instance is SATISFIABLE > Runtime Solver: 0.00506009s > Runtime decision procedure: 0.00510252s > Running propositional reduction > Solving with MiniSAT 2.2.1 with simplifier > 19821 variables, 7 clauses > SAT checker inconsistent: instance is UNSATISFIABLE > Runtime Solver: 5.39e-06s > Runtime decision procedure: 1.7616e-05s > > ** Results: > <builtin-library-fclose> function fclose > [fclose.precondition_instance.1] line 24 free argument must be NULL or valid > pointer: FAILURE > [fclose.precondition_instance.2] line 24 free argument must be dynamic > object: FAILURE > [fclose.precondition_instance.3] line 24 free argument has offset zero: > FAILURE > [fclose.precondition_instance.4] line 24 double free: SUCCESS > [fclose.precondition_instance.5] line 24 free called for new[] object: SUCCESS > [fclose.precondition_instance.6] line 24 free called for stack-allocated > object: SUCCESS > > <builtin-library-fgets> function fgets > [fgets.pointer_dereference.1] line 19 dereference failure: pointer NULL in > *stream: FAILURE > [fgets.pointer_dereference.2] line 19 dereference failure: pointer invalid in > *stream: FAILURE > [fgets.pointer_dereference.3] line 19 dereference failure: deallocated > dynamic object in *stream: FAILURE > [fgets.pointer_dereference.4] line 19 dereference failure: dead object in > *stream: FAILURE > [fgets.pointer_dereference.5] line 19 dereference failure: pointer outside > object bounds in *stream: FAILURE > [fgets.pointer_dereference.6] line 19 dereference failure: invalid integer > address in *stream: FAILURE > [fgets.assertion.1] line 32 buffer-overflow in fgets: SUCCESS > > main.c function main > [main.precondition_instance.1] line 17 strlen zero-termination: SUCCESS > > ** 9 of 14 failed (3 iterations) > VERIFICATION FAILED > > EXIT=10 > SIGNAL=0 > > > > Failed test.desc lines: > ^EXIT=0$ [FAILED] > ^VERIFICATION SUCCESSFUL$ [FAILED] > make[4]: *** [Makefile:13: test] Error 1 The full build log is available from: http://qa-logs.debian.net/2024/04/20/cbmc_5.95.1-4_unstable-armhf.log All bugs filed during this archive rebuild are listed at: https://bugs.debian.org/cgi-bin/pkgreport.cgi?tag=ftbfs-20240420;users=lu...@debian.org or: https://udd.debian.org/bugs/?release=na&merged=ign&fnewerval=7&flastmodval=7&fusertag=only&fusertagtag=ftbfs-20240420&fusertaguser=lu...@debian.org&allbugs=1&cseverity=1&ctags=1&caffected=1#results A list of current common problems and possible solutions is available at http://wiki.debian.org/qa.debian.org/FTBFS . You're welcome to contribute! If you reassign this bug to another package, please mark it as 'affects'-ing this package. See https://www.debian.org/Bugs/server-control#affects If you fail to reproduce this, please provide a build log and diff it with mine so that we can identify if something relevant changed in the meantime.
