Bug#1069438: marked as done (cbmc: FTBFS on armhf: make[4]: *** [Makefile:13: test] Error 1)

[Debian Bug Tracking System]

Your message dated Mon, 29 Apr 2024 14:36:56 +0000
with message-id <e1s1s7k-004t92...@fasolo.debian.org>
and subject line Bug#1069438: fixed in cbmc 5.95.1-5
has caused the Debian Bug report #1069438,
regarding cbmc: FTBFS on armhf: make[4]: *** [Makefile:13: test] Error 1
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ow...@bugs.debian.org
immediately.)


-- 
1069438: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1069438
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems

--- Begin Message ---

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  [OK] in 0 seconds
>   Running ACSL/quantifier-precedence.desc  [OK] in 0 seconds
>   Running ASHR1/test.desc  [OK] in 0 seconds
>   Running Address_of1/test.desc  [OK] in 0 seconds
>   Running Address_of2/test.desc  [OK] in 0 seconds
>   Running Anonymous_Struct1/test.desc  [OK] in 1 seconds
>   Running Anonymous_Struct2/test.desc  [OK] in 0 seconds
>   Running Anonymous_Struct3/test.desc  [OK] in 0 seconds
>   Running Array_Access1/test.desc  [OK] in 0 seconds
>   Running Array_Access2/test.desc  [OK] in 0 seconds
>   Running Array_Access3/test.desc  [OK] in 0 seconds
>   Running Array_Initialization1/test.desc  [OK] in 0 seconds
>   Running Array_Initialization2/test.desc  [OK] in 0 seconds
>   Running Array_Initialization3/test.desc  [OK] in 0 seconds
>   Running Array_Pointer1/test.desc  [OK] in 0 seconds
>   Running Array_Pointer2/test.desc  [OK] in 0 seconds
>   Running Array_Pointer3/test.desc  [OK] in 0 seconds
>   Running Array_Pointer4/test.desc  [OK] in 0 seconds
>   Running Array_Pointer5/test.desc  [OK] in 0 seconds
>   Running Array_Pointer6/test.desc  [OK] in 0 seconds
>   Running Array_Pointer7/test.desc  [OK] in 0 seconds
>   Running Array_Propagation1/test.desc  [OK] in 0 seconds
>   Running Array_UF1/test.desc  [OK] in 0 seconds
>   Running Array_UF10/test.desc  [OK] in 0 seconds
>   Running Array_UF11/test.desc  [OK] in 0 seconds
>   Running Array_UF12/test.desc  [OK] in 1 seconds
>   Running Array_UF13/test.desc  [OK] in 0 seconds
>   Running Array_UF14/test.desc  [OK] in 0 seconds
>   Running Array_UF15/test.desc  [OK] in 0 seconds
>   Running Array_UF16/test.desc  [OK] in 0 seconds
>   Running Array_UF17/test.desc  [OK] in 0 seconds
>   Running Array_UF18/test.desc  [OK] in 0 seconds
>   Running Array_UF19/test.desc  [OK] in 0 seconds
>   Running Array_UF2/test.desc  [OK] in 0 seconds
>   Running Array_UF20/test.desc  [OK] in 0 seconds
>   Running Array_UF21/test.desc  [OK] in 1 seconds
>   Running Array_UF22/test.desc  [SKIPPED]
>   Running Array_UF3/test.desc  [OK] in 0 seconds
>   Running Array_UF4/test.desc  [SKIPPED]
>   Running Array_UF5/test.desc  [OK] in 0 seconds
>   Running Array_UF6/test.desc  [OK] in 0 seconds
>   Running Array_UF7/test.desc  [OK] in 0 seconds
>   Running Array_UF8/test.desc  [SKIPPED]
>   Running Array_UF9/test.desc  [OK] in 0 seconds
>   Running Array_operations1/full-slice.desc  [OK] in 0 seconds
>   Running Array_operations1/test.desc  [OK] in 0 seconds
>   Running Array_operations2/test.desc  [OK] in 0 seconds
>   Running Associativity1/test.desc  [OK] in 0 seconds
>   Running Assumption1/test.desc  [OK] in 0 seconds
>   Running BV_Arithmetic1/test.desc  [OK] in 1 seconds
>   Running BV_Arithmetic2/test.desc  [OK] in 0 seconds
>   Running BV_Arithmetic3/test.desc  [OK] in 0 seconds
>   Running BV_Arithmetic4/test.desc  [OK] in 0 seconds
>   Running BV_Arithmetic5/test.desc  [OK] in 0 seconds
>   Running BV_Arithmetic6/test.desc  [OK] in 0 seconds
>   Running Bitfields1/test.desc  [OK] in 0 seconds
>   Running Bitfields2/test.desc  [OK] in 0 seconds
>   Running Bitfields3/paths.desc  [OK] in 1 seconds
>   Running Bitfields3/test.desc  [OK] in 0 seconds
>   Running Bitfields4/test.desc  [OK] in 0 seconds
>   Running Bool/bool1.desc  [OK] in 0 seconds
>   Running Bool/bool2.desc  [OK] in 0 seconds
>   Running Bool/bool3.desc  [OK] in 0 seconds
>   Running Bool/bool4.desc  [OK] in 0 seconds
>   Running Bool/bool5-full-slice.desc  [OK] in 0 seconds
>   Running Bool/bool5.desc  [OK] in 0 seconds
>   Running Bool/bool6.desc  [OK] in 1 seconds
>   Running Bool/bool7.desc  [SKIPPED]
>   Running Boolean_Guards1/test.desc  [OK] in 0 seconds
>   Running Computed-Goto1/test.desc  [OK] in 0 seconds
>   Running Division1/test.desc  [OK] in 0 seconds
>   Running Division2/test.desc  [OK] in 0 seconds
>   Running Ellipsis1/test.desc  [OK] in 0 seconds
>   Running Ellipsis2/test.desc  [OK] in 0 seconds
>   Running Empty_struct1/test.desc  [OK] in 0 seconds
>   Running Empty_struct2/test.desc  [OK] in 0 seconds
>   Running Empty_struct3/test.desc  [OK] in 0 seconds
>   Running End_thread1/test.desc  [OK] in 0 seconds
>   Running Endianness1/test.desc  [OK] in 0 seconds
>   Running Endianness2/test.desc  [OK] in 0 seconds
>   Running Endianness3/test.desc  [OK] in 0 seconds
>   Running Endianness4/test.desc  [OK] in 0 seconds
>   Running Endianness5/test.desc  [OK] in 0 seconds
>   Running Endianness6/test.desc  [OK] in 0 seconds
>   Running Endianness7/test.desc  [OK] in 0 seconds
>   Running Endianness8/test.desc  [OK] in 0 seconds
>   Running Endianness9/test.desc  [OK] in 0 seconds
>   Running Error_Label1/test.desc  [OK] in 0 seconds
>   Running Error_Label2/test.desc  [OK] in 0 seconds
>   Running Error_Label3/test.desc  [OK] in 0 seconds
>   Running Eval_Order1/test.desc  [OK] in 0 seconds
>   Running Eval_Order2/test.desc  [SKIPPED]
>   Running Exceptions1/test.desc  [OK] in 1 seconds
>   Running Failed_Symbols1/test.desc  [OK] in 0 seconds
>   Running Failing_Assert1/dimacs.desc  [OK] in 0 seconds
>   Running Failing_Assert1/external-z3.desc  [OK] in 0 seconds
>   Running Failing_Assert1/test.desc  [OK] in 0 seconds
>   Running Fixedbv1/test.desc  [OK] in 0 seconds
>   Running Fixedbv2/test.desc  [OK] in 0 seconds
>   Running Fixedbv3/test.desc  [OK] in 0 seconds
>   Running Fixedbv4/test.desc  [OK] in 0 seconds
>   Running Fixedbv5/test.desc  [OK] in 0 seconds
>   Running Fixedbv6/test.desc  [OK] in 0 seconds
>   Running Fixedbv7/test.desc  [SKIPPED]
>   Running Fixedbv8/test.desc  [OK] in 0 seconds
>   Running Float-div2/test.desc  [OK] in 0 seconds
>   Running Float-div3/test.desc  [OK] in 0 seconds
>   Running Float-equality1/test_equality.desc  [SKIPPED]
>   Running Float-equality1/test_no_equality.desc  [OK] in 0 seconds
>   Running Float-equality2/test.desc  [OK] in 0 seconds
>   Running Float-flags-no-simp1/test.desc  [OK] in 1 seconds
>   Running Float-flags-simp1/test.desc  [OK] in 0 seconds
>   Running Float-no-simp1/test.desc  [OK] in 0 seconds
>   Running Float-no-simp2/test.desc  [OK] in 2 seconds
>   Running Float-no-simp3/test.desc  [OK] in 0 seconds
>   Running Float-no-simp4/test.desc  [OK] in 0 seconds
>   Running Float-no-simp5/test.desc  [OK] in 0 seconds
>   Running Float-no-simp6/test.desc  [OK] in 0 seconds
>   Running Float-no-simp7/test.desc  [OK] in 0 seconds
>   Running Float-no-simp9/test.desc  [OK] in 0 seconds
>   Running Float-overflow1/test.desc  [OK] in 0 seconds
>   Running Float-overflow2/test.desc  [OK] in 0 seconds
>   Running Float-rounding/compile_time_rounding.desc  [OK] in 0 
> seconds
>   Running Float-rounding2/test.desc  [OK] in 0 seconds
>   Running Float-smt2-1/test.desc  [SKIPPED]
>   Running Float-to-double2/test.desc  [OK] in 1 seconds
>   Running Float-to-int1/test.desc  [OK] in 0 seconds
>   Running Float-to-int2/test.desc  [OK] in 0 seconds
>   Running Float-to-int3/test.desc  [OK] in 0 seconds
>   Running Float-zero-sum1/test.desc  [OK] in 0 seconds
>   Running Float1/test.desc  [OK] in 0 seconds
>   Running Float11/test.desc  [OK] in 0 seconds
>   Running Float12/test.desc  [OK] in 0 seconds
>   Running Float13/test.desc  [OK] in 0 seconds
>   Running Float14/test.desc  [OK] in 0 seconds
>   Running Float2/test.desc  [OK] in 0 seconds
>   Running Float20/test.desc  [OK] in 0 seconds
>   Running Float21/test.desc  [OK] in 1 seconds
>   Running Float22/test.desc  [OK] in 0 seconds
>   Running Float23/test.desc  [OK] in 0 seconds
>   Running Float24/test.desc  [OK] in 0 seconds
>   Running Float3/test.desc  [OK] in 0 seconds
>   Running Float4/test.desc  [OK] in 8 seconds
>   Running Float5/test.desc  [OK] in 0 seconds
>   Running Float6/test.desc  [OK] in 0 seconds
>   Running Float7/test.desc  [OK] in 0 seconds
>   Running Float8/smt.desc  [SKIPPED]
>   Running Float8/test.desc  [OK] in 0 seconds
>   Running Free1/test.desc  [OK] in 0 seconds
>   Running Free2/test.desc  [OK] in 0 seconds
>   Running Free3/test.desc  [OK] in 0 seconds
>   Running Free4/test.desc  [OK] in 1 seconds
>   Running Function-KnR1/test.desc  [OK] in 0 seconds
>   Running Function1/test.desc  [OK] in 0 seconds
>   Running Function10/test.desc  [OK] in 0 seconds
>   Running Function11/test.desc  [OK] in 0 seconds
>   Running Function12/test.desc  [OK] in 0 seconds
>   Running Function13/test.desc  [OK] in 0 seconds
>   Running Function14/test.desc  [OK] in 0 seconds
>   Running Function2/test.desc  [OK] in 0 seconds
>   Running Function3/test.desc  [OK] in 0 seconds
>   Running Function4/test.desc  [OK] in 0 seconds
>   Running Function5/test.desc  [OK] in 0 seconds
>   Running Function6/test.desc  [OK] in 0 seconds
>   Running Function7/test.desc  [OK] in 0 seconds
>   Running Function8/test.desc  [OK] in 0 seconds
>   Running Function9/test.desc  [OK] in 0 seconds
>   Running Function_Eval_Order1/test.desc  [SKIPPED]
>   Running Function_Eval_Order2/test.desc  [OK] in 0 seconds
>   Running Function_Parameters1/test.desc  [SKIPPED]
>   Running Function_Pointer1/test.desc  [OK] in 0 seconds
>   Running Function_Pointer10/test.desc  [OK] in 0 seconds
>   Running Function_Pointer11/test.desc  [OK] in 0 seconds
>   Running Function_Pointer12/test.desc  [OK] in 0 seconds
>   Running Function_Pointer13/test.desc  [OK] in 0 seconds
>   Running Function_Pointer14/test.desc  [OK] in 1 seconds
>   Running Function_Pointer15/test.desc  [OK] in 0 seconds
>   Running Function_Pointer16/test.desc  [OK] in 0 seconds
>   Running Function_Pointer17/test.desc  [OK] in 0 seconds
>   Running Function_Pointer18/test.desc  [OK] in 0 seconds
>   Running Function_Pointer19/test.desc  [OK] in 0 seconds
>   Running Function_Pointer2/test.desc  [OK] in 0 seconds
>   Running Function_Pointer3/test.desc  [OK] in 0 seconds
>   Running Function_Pointer4/test.desc  [OK] in 0 seconds
>   Running Function_Pointer5/test.desc  [OK] in 0 seconds
>   Running Function_Pointer6/test.desc  [OK] in 0 seconds
>   Running Function_Pointer7/test.desc  [OK] in 0 seconds
>   Running Function_Pointer8/test.desc  [OK] in 0 seconds
>   Running Function_Pointer9/test.desc  [OK] in 0 seconds
>   Running Function_Pointer_Init_No_Candidate/test.desc  [OK] in 0 
> seconds
>   Running Function_Pointer_Init_One_Candidate/test.desc  [OK] in 0 
> seconds
>   Running Function_Pointer_Init_Two_Candidates/test.desc  [OK] in 0 
> seconds
>   Running Global_Initialization1/test.desc  [OK] in 0 seconds
>   Running Global_Initialization2/test.desc  [OK] in 0 seconds
>   Running Initialization1/test.desc  [OK] in 0 seconds
>   Running Initialization2/test.desc  [OK] in 0 seconds
>   Running Initialization3/test.desc  [OK] in 0 seconds
>   Running Initialization5/test.desc  [OK] in 0 seconds
>   Running Initialization6/test.desc  [OK] in 0 seconds
>   Running Initialization7/test.desc  [OK] in 0 seconds
>   Running KnR1/test.desc  [OK] in 1 seconds
>   Running Linked_List1/test.desc  [OK] in 0 seconds
>   Running Linking1/test.desc  [OK] in 0 seconds
>   Running Linking2/test.desc  [OK] in 0 seconds
>   Running Linking3/test.desc  [OK] in 0 seconds
>   Running Linking4/test.desc  [OK] in 0 seconds
>   Running Linking5/test.desc  [OK] in 0 seconds
>   Running Linking6/test.desc  [OK] in 0 seconds
>   Running Linking7/member-name-mismatch.desc  [OK] in 0 seconds
>   Running Linking7/return_type.desc  [OK] in 0 seconds
>   Running Linking7/test.desc  [OK] in 0 seconds
>   Running Linking8/test.desc  [OK] in 0 seconds
>   Running Local_out_of_scope1/test.desc  [OK] in 0 seconds
>   Running Local_out_of_scope2/test.desc  [OK] in 0 seconds
>   Running Local_out_of_scope3/test.desc  [OK] in 0 seconds
>   Running Local_out_of_scope4/test.desc  [OK] in 0 seconds
>   Running Malloc1/test.desc  [OK] in 0 seconds
>   Running Malloc10/test.desc  [OK] in 1 seconds
>   Running Malloc11/slice-formula.desc  [OK] in 0 seconds
>   Running Malloc11/test.desc  [OK] in 0 seconds
>   Running Malloc12/test.desc  [SKIPPED]
>   Running Malloc13/test.desc  [OK] in 0 seconds
>   Running Malloc14/test.desc  [OK] in 0 seconds
>   Running Malloc15/test.desc  [OK] in 0 seconds
>   Running Malloc16/test.desc  [OK] in 0 seconds
>   Running Malloc17/test.desc  [OK] in 0 seconds
>   Running Malloc18/test.desc  [OK] in 0 seconds
>   Running Malloc19/test.desc  [OK] in 0 seconds
>   Running Malloc2/test.desc  [OK] in 0 seconds
>   Running Malloc21/test.desc  [OK] in 0 seconds
>   Running Malloc22/test.desc  [OK] in 0 seconds
>   Running Malloc23/test.desc  [OK] in 0 seconds
>   Running Malloc24/test.desc  [OK] in 1 seconds
>   Running Malloc25/test.desc  [OK] in 0 seconds
>   Running Malloc3/test.desc  [OK] in 0 seconds
>   Running Malloc4/test.desc  [OK] in 0 seconds
>   Running Malloc5/test.desc  [OK] in 0 seconds
>   Running Malloc6/test.desc  [OK] in 0 seconds
>   Running Malloc7/test.desc  [OK] in 0 seconds
>   Running Malloc8/test.desc  [OK] in 0 seconds
>   Running Malloc9/test.desc  [OK] in 0 seconds
>   Running Memory_leak1/test.desc  [OK] in 0 seconds
>   Running Memory_leak2/test.desc  [OK] in 0 seconds
>   Running Memory_leak_abort/test.desc  [OK] in 1 seconds
>   Running Minisat_Simp1/test.desc  [OK] in 0 seconds
>   Running Mod1/test.desc  [OK] in 0 seconds
>   Running Mod2/test.desc  [OK] in 0 seconds
>   Running Multi_Dimensional_Array1/test.desc  [OK] in 0 seconds
>   Running Multi_Dimensional_Array2/test.desc  [OK] in 0 seconds
>   Running Multi_Dimensional_Array3/test.desc  [OK] in 0 seconds
>   Running Multi_Dimensional_Array4/test.desc  [OK] in 0 seconds
>   Running Multi_Dimensional_Array5/test.desc  [OK] in 0 seconds
>   Running Multi_Dimensional_Array6/test.desc  [OK] in 0 seconds
>   Running Multiple_Properties1/test.desc  [OK] in 0 seconds
>   Running Negation1/test.desc  [OK] in 1 seconds
>   Running Negation2/test.desc  [OK] in 0 seconds
>   Running Nondet1/test.desc  [OK] in 0 seconds
>   Running Pointer1/test.desc  [OK] in 0 seconds
>   Running Pointer10/test.desc  [OK] in 0 seconds
>   Running Pointer11/test.desc  [OK] in 0 seconds
>   Running Pointer12/test.desc  [OK] in 0 seconds
>   Running Pointer14/test.desc  [OK] in 0 seconds
>   Running Pointer15/test.desc  [OK] in 0 seconds
>   Running Pointer17/test.desc  [OK] in 0 seconds
>   Running Pointer18/full-slice.desc  [OK] in 0 seconds
>   Running Pointer18/test.desc  [OK] in 0 seconds
>   Running Pointer2/test.desc  [OK] in 0 seconds
>   Running Pointer20/test.desc  [OK] in 0 seconds
>   Running Pointer21/test.desc  [OK] in 0 seconds
>   Running Pointer23/test.desc  [OK] in 0 seconds
>   Running Pointer24/test.desc  [OK] in 0 seconds
>   Running Pointer25/test.desc  [OK] in 0 seconds
>   Running Pointer26/test.desc  [OK] in 0 seconds
>   Running Pointer27/test.desc  [OK] in 0 seconds
>   Running Pointer28/test.desc  [OK] in 0 seconds
>   Running Pointer29/test.desc  [OK] in 0 seconds
>   Running Pointer3/test.desc  [OK] in 1 seconds
>   Running Pointer30/test.desc  [OK] in 0 seconds
>   Running Pointer31/test.desc  [OK] in 0 seconds
>   Running Pointer4/test.desc  [OK] in 0 seconds
>   Running Pointer6/test.desc  [OK] in 0 seconds
>   Running Pointer7/test.desc  [OK] in 0 seconds
>   Running Pointer8/test.desc  [OK] in 0 seconds
>   Running Pointer9/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic1/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic10/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic11/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic12/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic13/test.desc  [SKIPPED]
>   Running Pointer_Arithmetic14/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic15/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic16/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic17/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic18/test.desc  [SKIPPED]
>   Running Pointer_Arithmetic19/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic2/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic3/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic4/test.desc  [OK] in 1 seconds
>   Running Pointer_Arithmetic5/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic6/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic7/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic8/test.desc  [OK] in 0 seconds
>   Running Pointer_Arithmetic9/test.desc  [OK] in 0 seconds
>   Running Pointer_Assume1/test.desc  [OK] in 0 seconds
>   Running Pointer_Object_Type1/test.desc  [OK] in 0 seconds
>   Running Pointer_array1/test.desc  [OK] in 0 seconds
>   Running Pointer_array2/test.desc  [OK] in 0 seconds
>   Running Pointer_array3/test.desc  [OK] in 0 seconds
>   Running Pointer_array4/test.desc  [OK] in 0 seconds
>   Running Pointer_array5/test.desc  [OK] in 0 seconds
>   Running Pointer_array6/test.desc  [SKIPPED]
>   Running Pointer_array7/big-endian.desc  [OK] in 0 seconds
>   Running Pointer_array7/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract1/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract2/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract3/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract4/program-only.desc  [OK] in 1 seconds
>   Running Pointer_byte_extract4/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract5/no-simplify.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract5/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract6/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract7/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract8/test.desc  [OK] in 0 seconds
>   Running Pointer_byte_extract9/test.desc  [OK] in 0 seconds
>   Running Pointer_comparison1/test.desc  [SKIPPED]
>   Running Pointer_comparison2/test.desc  [OK] in 0 seconds
>   Running Pointer_comparison3/test.desc  [OK] in 0 seconds
>   Running Pointer_comparison4/test.desc  [OK] in 0 seconds
>   Running Pointer_comparison5/test.desc  [OK] in 0 seconds
>   Running Pointer_difference1/no-simplify.desc  [OK] in 0 seconds
>   Running Pointer_difference1/test.desc  [OK] in 0 seconds
>   Running Pointer_difference2/test.desc  [OK] in 0 seconds
>   Running Promotion1/test.desc  [OK] in 0 seconds
>   Running Promotion2/test.desc  [OK] in 0 seconds
>   Running Promotion3/test.desc  [OK] in 0 seconds
>   Running Promotion4/test.desc  [OK] in 0 seconds
>   Running Quantifiers-assertion/test.desc  [OK] in 1 seconds
>   Running Quantifiers-assignment/test.desc  [OK] in 0 seconds
>   Running Quantifiers-copy/test.desc  [OK] in 0 seconds
>   Running Quantifiers-expr-cleaning/test.desc  [OK] in 0 seconds
>   Running Quantifiers-if/test.desc  [OK] in 0 seconds
>   Running Quantifiers-initialisation/test.desc  [OK] in 0 seconds
>   Running Quantifiers-initialisation2/test.desc  [OK] in 0 seconds
>   Running Quantifiers-invalid-var-range/test.desc  [SKIPPED]
>   Running Quantifiers-not/test.desc  [OK] in 0 seconds
>   Running Quantifiers-not-exists/fixed.desc  [OK] in 0 seconds
>   Running Quantifiers-simplify/rewrite_exists.desc  [OK] in 0 seconds
>   Running Quantifiers-simplify/rewrite_forall.desc  [OK] in 0 seconds
>   Running Quantifiers-simplify/simplify_not_forall.desc  [OK] in 0 
> seconds
>   Running Quantifiers-simplify/test.desc  [SKIPPED]
>   Running Quantifiers-two-dimension-array/fixed.desc  [OK] in 0 
> seconds
>   Running Quantifiers-two-dimension-array/test.desc  [OK] in 0 
> seconds
>   Running Quantifiers-type/test.desc  [SKIPPED]
>   Running Quantifiers-type2/test.desc  [OK] in 0 seconds
>   Running Quantifiers1/quantifier-with-side-effect.desc  [OK] in 0 
> seconds
>   Running Quantifiers1/test.desc  [OK] in 0 seconds
>   Running Recursion1/test.desc  [OK] in 0 seconds
>   Running Recursion2/test.desc  [OK] in 0 seconds
>   Running Recursion3/test.desc  [OK] in 0 seconds
>   Running Recursion4/test.desc  [OK] in 1 seconds
>   Running Recursion5/test.desc  [OK] in 0 seconds
>   Running Recursion6/test.desc  [OK] in 0 seconds
>   Running SIMD1/test.desc  [SKIPPED]
>   Running Same_Basename1/test.desc  [OK] in 0 seconds
>   Running Sideeffects1/test.desc  [OK] in 0 seconds
>   Running Sideeffects2/test.desc  [OK] in 0 seconds
>   Running Sideeffects3/test.desc  [OK] in 0 seconds
>   Running Sideeffects4/test.desc  [OK] in 0 seconds
>   Running Sideeffects5/test.desc  [OK] in 0 seconds
>   Running Sideeffects6/test.desc  [OK] in 0 seconds
>   Running Sideeffects7/test.desc  [OK] in 0 seconds
>   Running Sideeffects8/test.desc  [OK] in 0 seconds
>   Running Sizeof1/test.desc  [OK] in 0 seconds
>   Running Static2/test.desc  [OK] in 0 seconds
>   Running Static4/test.desc  [OK] in 0 seconds
>   Running Static_Functions1/test.desc  [OK] in 0 seconds
>   Running String1/test.desc  [OK] in 0 seconds
>   Running String2/test.desc  [OK] in 0 seconds
>   Running String3/test.desc  [SKIPPED]
>   Running String4/test.desc  [OK] in 0 seconds
>   Running String5/test.desc  [OK] in 0 seconds
>   Running String7/test.desc  [OK] in 0 seconds
>   Running String8/test.desc  [OK] in 0 seconds
>   Running String_Abstraction1/test.desc  [OK] in 1 seconds
>   Running String_Abstraction10/test.desc  [SKIPPED]
>   Running String_Abstraction11/test.desc  [OK] in 0 seconds
>   Running String_Abstraction12/test.desc  [OK] in 0 seconds
>   Running String_Abstraction13/test.desc  [OK] in 0 seconds
>   Running String_Abstraction14/test.desc  [OK] in 0 seconds
>   Running String_Abstraction15/test.desc  [OK] in 0 seconds
>   Running String_Abstraction16/test.desc  [OK] in 0 seconds
>   Running String_Abstraction17/test.desc  [OK] in 0 seconds
>   Running String_Abstraction18/test.desc  [OK] in 0 seconds
>   Running String_Abstraction19/test.desc  [OK] in 0 seconds
>   Running String_Abstraction2/test.desc  [OK] in 0 seconds
>   Running String_Abstraction20/test.desc  [OK] in 1 seconds
>   Running String_Abstraction21/test.desc  [OK] in 0 seconds
>   Running String_Abstraction22/test.desc  [OK] in 0 seconds
>   Running String_Abstraction23/test.desc  [OK] in 0 seconds
>   Running String_Abstraction24/test.desc  [OK] in 0 seconds
>   Running String_Abstraction3/test.desc  [OK] in 0 seconds
>   Running String_Abstraction4/test.desc  [OK] in 0 seconds
>   Running String_Abstraction5/test.desc  [OK] in 0 seconds
>   Running String_Abstraction6/test.desc  [SKIPPED]
>   Running String_Abstraction7/test.desc  [FAILED]
>   Running String_Abstraction8/test.desc  [OK] in 0 seconds
>   Running String_Abstraction9/test.desc  [OK] in 0 seconds
>   Running String_Literal1/test.desc  [OK] in 0 seconds
>   Running Struct_Array1/test.desc  [OK] in 0 seconds
>   Running Struct_Bytewise1/test.desc  [OK] in 0 seconds
>   Running Struct_Bytewise2/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization1/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization10/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization2/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization3/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization4/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization5/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization6/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization7/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization8/test.desc  [OK] in 0 seconds
>   Running Struct_Initialization9/test.desc  [OK] in 0 seconds
>   Running Struct_Padding1/test.desc  [OK] in 0 seconds
>   Running Struct_Pointer1/test.desc  [OK] in 0 seconds
>   Running Struct_Pointer2/test.desc  [OK] in 1 seconds
>   Running Struct_Pointer3/test.desc  [OK] in 0 seconds
>   Running Struct_Pointer_Array1/test.desc  [OK] in 0 seconds
>   Running Struct_Propagation1/test.desc  [OK] in 0 seconds
>   Running Type_Error1/test.desc  [OK] in 0 seconds
>   Running Typecast1/test.desc  [OK] in 0 seconds
>   Running Typecast2/test.desc  [OK] in 0 seconds
>   Running Typecast3/test.desc  [OK] in 0 seconds
>   Running Unbounded_Array1/test.desc  [OK] in 0 seconds
>   Running Unbounded_Array2/test.desc  [OK] in 0 seconds
>   Running Unbounded_Array3/test.desc  [OK] in 0 seconds
>   Running Unbounded_Array4/test.desc  [OK] in 0 seconds
>   Running Unbounded_Array5/test.desc  [OK] in 0 seconds
>   Running Unbounded_Array6/test.desc  [OK] in 0 seconds
>   Running Undefined_Function1/test.desc  [OK] in 0 seconds
>   Running Undefined_Function2/test.desc  [OK] in 0 seconds
>   Running Undefined_Shift1/test.desc  [OK] in 0 seconds
>   Running Union_Initialization1/test.desc  [OK] in 0 seconds
>   Running Union_Initialization2/test.desc  [OK] in 0 seconds
>   Running Union_Initialization5/test.desc  [OK] in 0 seconds
>   Running Unwinding_Assertions_Improved1/test.desc  [SKIPPED]
>   Running Unwinding_Locality1/test.desc  [OK] in 0 seconds
>   Running Variadic1/test.desc  [OK] in 0 seconds
>   Running Visual_Studio_Types1/test.desc  [OK] in 0 seconds
>   Running Visual_Studio_Types2/test.desc  [OK] in 0 seconds
>   Running Volatile1/test.desc  [SKIPPED]
>   Running Zero_Initialization1/test.desc  [OK] in 1 seconds
>   Running __builtin_clz-01/big-endian.desc  [OK] in 0 seconds
>   Running __builtin_clz-01/test.desc  [OK] in 0 seconds
>   Running __builtin_ctz-01/big-endian.desc  [OK] in 0 seconds
>   Running __builtin_ctz-01/test.desc  [OK] in 0 seconds
>   Running __builtin_ffs-01/big-endian.desc  [OK] in 0 seconds
>   Running __builtin_ffs-01/test.desc  [OK] in 0 seconds
>   Running __func__1/test.desc  [OK] in 0 seconds
>   Running address_of_struct_member/test.desc  [OK] in 0 seconds
>   Running address_of_struct_member_rec/test.desc  [OK] in 0 seconds
>   Running address_space_size_limit1/test.desc  [OK] in 5 seconds
>   Running address_space_size_limit2/test.desc  [SKIPPED]
>   Running address_space_size_limit3/test.desc  [OK] in 10 seconds
>   Running always_inline1/test.desc  [OK] in 0 seconds
>   Running always_inline2/test.desc  [OK] in 0 seconds
>   Running always_inline3/test.desc  [OK] in 0 seconds
>   Running apply_condition1/test.desc  [OK] in 0 seconds
>   Running argc-and-argv/argc1.desc  [OK] in 0 seconds
>   Running argc-and-argv/argv1.desc  [OK] in 0 seconds
>   Running argv2/test.desc  [OK] in 0 seconds
>   Running array-bug-6230/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity1/test.desc  [OK] in 1 seconds
>   Running array-cell-sensitivity1/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity10/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity10/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity11/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity11/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity12/test.desc  [SKIPPED]
>   Running array-cell-sensitivity12/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity13/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity13/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity14/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity14/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity15/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity2/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity2/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity3/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity3/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity4/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity4/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity5/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity5/test_execution.desc  [OK] in 1 
> seconds
>   Running array-cell-sensitivity6/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity6/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity7/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity7/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity8/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity8/test_execution.desc  [OK] in 0 
> seconds
>   Running array-cell-sensitivity9/test.desc  [OK] in 0 seconds
>   Running array-cell-sensitivity9/test_execution.desc  [OK] in 0 
> seconds
>   Running array-constraint/test.desc  [OK] in 0 seconds
>   Running array-constraint/test_json.desc  [SKIPPED]
>   Running array-constraint/test_xml.desc  [OK] in 0 seconds
>   Running array-function-parameters/test.desc  [OK] in 0 seconds
>   Running array-tests/test.desc  [OK] in 1 seconds
>   Running array-tests/uf-always.desc  [OK] in 1 seconds
>   Running array-tests/zero-sized.desc  [OK] in 0 seconds
>   Running array_constraints1/test.desc  [OK] in 0 seconds
>   Running array_of_bool_as_bitvec/test-smt2-outfile.desc  [OK] in 0 
> seconds
>   Running assert_func_four/test.desc  [OK] in 0 seconds
>   Running assert_lhs/test.desc  [OK] in 0 seconds
>   Running assert_one/test.desc  [OK] in 0 seconds
>   Running assert_rtn_four/test.desc  [OK] in 0 seconds
>   Running assigning_nullpointers_should_not_crash_symex/test.desc  
> [OK] in 0 seconds
>   Running atomic_X_fetch-1/pointer.desc  [OK] in 0 seconds
>   Running atomic_X_fetch-1/test.desc  [OK] in 0 seconds
>   Running atomic_X_fetch-1/two.desc  [OK] in 0 seconds
>   Running atomic_fetch_X-1/pointer.desc  [OK] in 0 seconds
>   Running atomic_fetch_X-1/test.desc  [OK] in 0 seconds
>   Running atomic_fetch_X-1/two.desc  [OK] in 0 seconds
>   Running atomic_load_store-1/test.desc  [OK] in 0 seconds
>   Running atomic_section_seq1/test.desc  [OK] in 0 seconds
>   Running aws-byte-buf-regression/test.desc  [OK] in 0 seconds
>   Running bad_option/test.desc  [OK] in 0 seconds
>   Running bad_option/test_multiple.desc  [OK] in 0 seconds
>   Running big-endian-array1/test.desc  [OK] in 1 seconds
>   Running bounds_check1/test.desc  [OK] in 3 seconds
>   Running bounds_check2/test.desc  [OK] in 0 seconds
>   Running byte-op-metric/test.desc  [OK] in 0 seconds
>   Running byte-op-metric/test_json.desc  [OK] in 0 seconds
>   Running byte_extract1/test.desc  [OK] in 0 seconds
>   Running byte_extract2/test.desc  [OK] in 0 seconds
>   Running byte_update1/test.desc  [OK] in 0 seconds
>   Running byte_update10/test.desc  [OK] in 0 seconds
>   Running byte_update11/test.desc  [OK] in 0 seconds
>   Running byte_update12/test.desc  [OK] in 0 seconds
>   Running byte_update13/test.desc  [OK] in 1 seconds
>   Running byte_update14/test.desc  [OK] in 0 seconds
>   Running byte_update15/test.desc  [OK] in 0 seconds
>   Running byte_update16/big-endian.desc  [OK] in 0 seconds
>   Running byte_update16/little-endian.desc  [OK] in 0 seconds
>   Running byte_update17/test.desc  [OK] in 0 seconds
>   Running byte_update18/test.desc  [OK] in 0 seconds
>   Running byte_update2/test.desc  [OK] in 0 seconds
>   Running byte_update3/test.desc  [OK] in 0 seconds
>   Running byte_update4/test.desc  [OK] in 0 seconds
>   Running byte_update5/full-slice.desc  [OK] in 0 seconds
>   Running byte_update5/test.desc  [OK] in 0 seconds
>   Running byte_update6/test.desc  [OK] in 0 seconds
>   Running byte_update7/test.desc  [OK] in 1 seconds
>   Running byte_update8/test.desc  [OK] in 0 seconds
>   Running byte_update9/test.desc  [OK] in 0 seconds
>   Running c99_Bool/test.desc  [OK] in 0 seconds
>   Running char1/test.desc  [OK] in 0 seconds
>   Running character_handling1/test.desc  [OK] in 0 seconds
>   Running clang_builtins/bitreverse-typeconflict.desc  [OK] in 0 
> seconds
>   Running clang_builtins/bitreverse.desc  [OK] in 0 seconds
>   Running clang_builtins/rotate.desc  [OK] in 0 seconds
>   Running comma1/test.desc  [OK] in 0 seconds
>   Running compact-trace/test.desc  [OK] in 0 seconds
>   Running complex1/test.desc  [OK] in 0 seconds
>   Running compound-assignment/compound_promotion.desc  [OK] in 0 
> seconds
>   Running compound_literal1/test.desc  [OK] in 0 seconds
>   Running condition-propagation-1/test.desc  [OK] in 0 seconds
>   Running condition-propagation-2/test.desc  [OK] in 0 seconds
>   Running condition-propagation-3/test.desc  [OK] in 0 seconds
>   Running condition-propagation-4/test.desc  [OK] in 0 seconds
>   Running const_ptr1/test.desc  [OK] in 0 seconds
>   Running constant_folding1/test.desc  [OK] in 1 seconds
>   Running constant_folding2/test.desc  [OK] in 0 seconds
>   Running constant_folding3/test.desc  [OK] in 0 seconds
>   Running constructor1/test.desc  [OK] in 0 seconds
>   Running constructor2/test.desc  [OK] in 0 seconds
>   Running cover-failed-assertions/test-no-failed-assertions.desc  
> [OK] in 0 seconds
>   Running cover-failed-assertions/test.desc  [OK] in 0 seconds
>   Running coverage_report1/paths.desc  [OK] in 0 seconds
>   Running coverage_report1/test.desc  [OK] in 0 seconds
>   Running coverage_report2/test.desc  [OK] in 0 seconds
>   Running cprover_assert_lhs/test.desc  [SKIPPED]
>   Running cprover_assert_two/test.desc  [OK] in 0 seconds
>   Running cprover_bool1/test.desc  [OK] in 0 seconds
>   Running cprover_fence_one/test.desc  [OK] in 0 seconds
>   Running cprover_havoc_object_lhs/test.desc  [SKIPPED]
>   Running cprover_havoc_object_one/test.desc  [OK] in 0 seconds
>   Running cprover_id1/test.desc  [OK] in 0 seconds
>   Running cprover_input_lhs/test.desc  [SKIPPED]
>   Running cprover_output_lhs/test.desc  [SKIPPED]
>   Running cprover_postcondition/test.desc  [OK] in 0 seconds
>   Running cprover_precondition/test.desc  [OK] in 0 seconds
>   Running dereference-cache-flag/test-no-cache.desc  [OK] in 0 
> seconds
>   Running dereference-cache-flag/test-with-cache.desc  [OK] in 0 
> seconds
>   Running destructor1/test.desc  [OK] in 0 seconds
>   Running destructors/compound_literal.desc  [OK] in 0 seconds
>   Running destructors/enter_lexical_block.desc  [OK] in 0 seconds
>   Running divide-by-one-simplify/test.desc  [OK] in 2 seconds
>   Running double_deref/double_deref.desc  [OK] in 0 seconds
>   Running double_deref/double_deref_single_alias.desc  [OK] in 0 
> seconds
>   Running double_deref/double_deref_with_cast.desc  [OK] in 0 seconds
>   Running double_deref/double_deref_with_cast_single_alias.desc  
> [OK] in 0 seconds
>   Running double_deref/double_deref_with_member.desc  [OK] in 0 
> seconds
>   Running double_deref/double_deref_with_member_single_alias.desc  
> [OK] in 1 seconds
>   Running double_deref/double_deref_with_pointer_arithmetic.desc  
> [OK] in 0 seconds
>   Running double_deref/double_deref_with_pointer_arithmetic_single_alias.desc 
>  [OK] in 0 seconds
>   Running dynamic_size1/stack_object.desc  [OK] in 0 seconds
>   Running dynamic_size1/test.desc  [OK] in 0 seconds
>   Running dynamic_sizeof1/test.desc  [OK] in 0 seconds
>   Running empty_compound_type1/test.desc  [OK] in 0 seconds
>   Running empty_compound_type2/test.desc  [OK] in 0 seconds
>   Running empty_compound_type3/test.desc  [OK] in 0 seconds
>   Running empty_compound_type4/test.desc  [OK] in 0 seconds
>   Running enum-trace1/test_json.desc  [OK] in 0 seconds
>   Running enum-trace1/test_xml.desc  [OK] in 0 seconds
>   Running enum1/test.desc  [OK] in 0 seconds
>   Running enum2/test.desc  [OK] in 0 seconds
>   Running enum3/test.desc  [OK] in 0 seconds
>   Running enum4/test.desc  [OK] in 0 seconds
>   Running enum5/test.desc  [OK] in 0 seconds
>   Running enum6/test.desc  [OK] in 0 seconds
>   Running enum7/test.desc  [OK] in 0 seconds
>   Running enum8/test.desc  [OK] in 1 seconds
>   Running enum9/test.desc  [OK] in 0 seconds
>   Running enum_is_in_range/enum_test3-simplified.desc  [OK] in 0 
> seconds
>   Running enum_is_in_range/enum_test3.desc  [OK] in 0 seconds
>   Running enum_is_in_range/enum_test4.desc  [OK] in 0 seconds
>   Running enum_is_in_range/enum_test5.desc  [OK] in 0 seconds
>   Running enum_is_in_range/enum_test7.desc  [OK] in 0 seconds
>   Running enum_is_in_range/enum_test8.desc  [OK] in 0 seconds
>   Running enum_is_in_range/format.desc  [OK] in 0 seconds
>   Running enum_is_in_range/no_duplicate.desc  [OK] in 0 seconds
>   Running enum_underlying_type_01/test.desc  [OK] in 0 seconds
>   Running enum_underlying_type_02/test.desc  [OK] in 0 seconds
>   Running enum_underlying_type_03/test.desc  [OK] in 0 seconds
>   Running equality_through_array1/test.desc  [OK] in 0 seconds
>   Running equality_through_array2/test.desc  [OK] in 0 seconds
>   Running equality_through_array3/test.desc  [OK] in 0 seconds
>   Running equality_through_array4/test.desc  [OK] in 0 seconds
>   Running equality_through_array5/test.desc  [OK] in 0 seconds
>   Running equality_through_array6/test.desc  [OK] in 0 seconds
>   Running equality_through_array_of_struct1/test.desc  [OK] in 0 
> seconds
>   Running equality_through_array_of_struct2/test.desc  [OK] in 0 
> seconds
>   Running equality_through_array_of_struct3/test.desc  [OK] in 0 
> seconds
>   Running equality_through_array_of_struct4/test.desc  [OK] in 1 
> seconds
>   Running equality_through_struct1/test.desc  [OK] in 0 seconds
>   Running equality_through_struct2/test.desc  [OK] in 0 seconds
>   Running equality_through_struct3/test.desc  [OK] in 0 seconds
>   Running equality_through_struct4/test.desc  [OK] in 0 seconds
>   Running equality_through_struct_containing_arrays1/test.desc  [OK] 
> in 0 seconds
>   Running equality_through_struct_containing_arrays2/test.desc  [OK] 
> in 0 seconds
>   Running equality_through_union1/test.desc  [OK] in 0 seconds
>   Running equality_through_union2/test.desc  [OK] in 0 seconds
>   Running equality_through_union3/test.desc  [OK] in 0 seconds
>   Running exit1/test.desc  [OK] in 0 seconds
>   Running export-symex-ready-goto/test-bad-usage.desc  [OK] in 0 
> seconds
>   Running export-symex-ready-goto/test-correct.desc  [OK] in 0 
> seconds
>   Running extern1/test.desc  [OK] in 0 seconds
>   Running extern2/test.desc  [OK] in 0 seconds
>   Running extern3/test.desc  [OK] in 0 seconds
>   Running extern4/test.desc  [OK] in 0 seconds
>   Running extern5/test.desc  [OK] in 0 seconds
>   Running extern_initialization1/test.desc  [OK] in 0 seconds
>   Running extern_initialization2/test.desc  [OK] 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  [OK] in 0 
> seconds
>   Running field-sensitivity-trace-wrong-counterexample-1/test.desc  
> [OK] in 0 seconds
>   Running field-sensitivity1/test.desc  [OK] in 1 seconds
>   Running field-sensitivity10/test.desc  [OK] in 0 seconds
>   Running field-sensitivity11/test.desc  [OK] in 0 seconds
>   Running field-sensitivity12/test.desc  [OK] in 0 seconds
>   Running field-sensitivity13/test.desc  [OK] in 0 seconds
>   Running field-sensitivity14/test.desc  [OK] in 0 seconds
>   Running field-sensitivity15/test.desc  [OK] in 0 seconds
>   Running field-sensitivity16/test.desc  [OK] in 0 seconds
>   Running field-sensitivity2/test.desc  [OK] in 0 seconds
>   Running field-sensitivity3/test.desc  [OK] in 0 seconds
>   Running field-sensitivity4/test.desc  [SKIPPED]
>   Running field-sensitivity5/test.desc  [OK] in 0 seconds
>   Running field-sensitivity6/test.desc  [OK] in 0 seconds
>   Running field-sensitivity7/test.desc  [OK] in 0 seconds
>   Running field-sensitivity8/test.desc  [OK] in 0 seconds
>   Running field-sensitivity9/test.desc  [OK] in 0 seconds
>   Running float-nan-check/test.desc  [OK] in 1 seconds
>   Running fmod1/test.desc  [OK] in 0 seconds
>   Running for-break1/test.desc  [OK] in 0 seconds
>   Running for1/test.desc  [OK] in 0 seconds
>   Running for2/test.desc  [OK] in 0 seconds
>   Running for3/test.desc  [OK] in 0 seconds
>   Running full_slice1/test.desc  [OK] in 0 seconds
>   Running full_slice2/test.desc  [OK] in 0 seconds
>   Running full_slice3/test.desc  [OK] in 0 seconds
>   Running function-return-no-body1/test.desc  [OK] in 0 seconds
>   Running function_not_found/test.desc  [SKIPPED]
>   Running function_option1/test.desc  [OK] in 0 seconds
>   Running gcc_attribute_alias1/test.desc  [OK] in 0 seconds
>   Running gcc_bswap1/test.desc  [OK] in 0 seconds
>   Running gcc_builtin_add_overflow/test.desc  [OK] in 0 seconds
>   Running gcc_builtin_add_overflow/type-conflict-2.desc  [OK] in 0 
> seconds
>   Running gcc_builtin_add_overflow/type-conflict.desc  [OK] in 0 
> seconds
>   Running gcc_builtin_mul_overflow/test.desc  [OK] in 1 seconds
>   Running gcc_builtin_sub_overflow/simplify.desc  [OK] in 0 seconds
>   Running gcc_builtin_sub_overflow/test.desc  [OK] in 0 seconds
>   Running gcc_builtin_va_arg_one/test.desc  [OK] in 0 seconds
>   Running gcc_c99-bool-1/test.desc  [OK] in 0 seconds
>   Running gcc_conditional_expr1/test.desc  [OK] in 0 seconds
>   Running gcc_local_label1/test.desc  [OK] in 0 seconds
>   Running gcc_popcount1/test.desc  [OK] in 1 seconds
>   Running gcc_popcount2/test.desc  [SKIPPED]
>   Running gcc_statement_expression1/test.desc  [OK] in 0 seconds
>   Running gcc_statement_expression2/test.desc  [OK] in 1 seconds
>   Running gcc_statement_expression3/test.desc  [OK] in 0 seconds
>   Running gcc_statement_expression4/test.desc  [OK] in 0 seconds
>   Running gcc_statement_expression5/test.desc  [OK] in 0 seconds
>   Running gcc_switch_case_range1/test.desc  [OK] in 0 seconds
>   Running gcc_switch_case_range2/test.desc  [OK] in 0 seconds
>   Running gcc_vector1/test.desc  [OK] in 0 seconds
>   Running gcc_vector2/test.desc  [OK] in 0 seconds
>   Running gcc_vector3/test.desc  [OK] in 0 seconds
>   Running goto1/test.desc  [OK] in 0 seconds
>   Running goto2/test.desc  [OK] in 0 seconds
>   Running goto3/test.desc  [OK] in 0 seconds
>   Running goto4/test.desc  [OK] in 0 seconds
>   Running goto5/test.desc  [OK] in 0 seconds
>   Running graphml_witness1/test.desc  [OK] in 0 seconds
>   Running graphml_witness2/test.desc  [OK] in 0 seconds
>   Running guard1/test.desc  [OK] in 0 seconds
>   Running havoc_choice/test.desc  [OK] in 0 seconds
>   Running havoc_object1/full-slice.desc  [OK] in 0 seconds
>   Running havoc_object1/test.desc  [OK] in 0 seconds
>   Running havoc_slice/test_array_slice_1.desc  [OK] in 1 seconds
>   Running havoc_slice/test_array_slice_2.desc  [OK] in 0 seconds
>   Running havoc_slice/test_array_symbolic_size.desc  [OK] in 0 
> seconds
>   Running havoc_slice/test_nondet_conditional.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_a.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_b.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_b_slice.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_c.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_d.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_raw_bytes.desc  [SKIPPED]
>   Running havoc_slice/test_struct_union_a.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_union_b.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_union_b_slice.desc  [OK] in 0 
> seconds
>   Running havoc_slice/test_struct_union_c.desc  [OK] in 0 seconds
>   Running havoc_slice/test_struct_union_d.desc  [OK] in 0 seconds
>   Running havoc_slice/test_whole_array.desc  [OK] in 1 seconds
>   Running havoc_slice/test_whole_array_with_offset.desc  [OK] in 0 
> seconds
>   Running havoc_slice_checks/full-slice.desc  [OK] in 0 seconds
>   Running havoc_slice_checks/test.desc  [OK] in 0 seconds
>   Running havoc_undefined_functions/test.desc  [OK] in 0 seconds
>   Running hex_string1/test.desc  [OK] in 0 seconds
>   Running hex_trace/test.desc  [OK] in 0 seconds
>   Running if1/test.desc  [OK] in 0 seconds
>   Running if2/test.desc  [OK] in 0 seconds
>   Running if3/test.desc  [OK] in 0 seconds
>   Running if4/test.desc  [OK] in 0 seconds
>   Running incomplete-sizeof/array.desc  [OK] in 0 seconds
>   Running incomplete-sizeof/enum.desc  [OK] in 0 seconds
>   Running incomplete-sizeof/struct.desc  [OK] in 0 seconds
>   Running incomplete-sizeof/union.desc  [OK] in 0 seconds
>   Running incomplete-structs/test.desc  [OK] in 0 seconds
>   Running inequality-with-constant-normalisation/test.desc  [OK] in 
> 0 seconds
>   Running inequality-with-constant-normalisation1/test.desc  [OK] in 
> 0 seconds
>   Running inline1/test.desc  [OK] in 1 seconds
>   Running integer-assignments1/integer-typecheck.desc  [OK] in 0 
> seconds
>   Running integer-assignments1/test.desc  [SKIPPED]
>   Running integer-pointer/test.desc  [SKIPPED]
>   Running integral-trace/test.desc  [OK] 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  [OK] in 0 seconds
>   Running json-interface1/test_wrong_flag.desc  [OK] in 0 seconds
>   Running json-interface1/test_wrong_option.desc  [OK] in 0 seconds
>   Running json-ui/no_entry.desc  [OK] in 0 seconds
>   Running json-ui/syntax_error.desc  [OK] in 0 seconds
>   Running json1/test.desc  [OK] in 0 seconds
>   Running lhs-pointer-aliases-constant/test.desc  [OK] in 0 seconds
>   Running link_json_symtabs/test.desc  [OK] in 0 seconds
>   Running little-endian-array1/test.desc  [OK] in 0 seconds
>   Running locations1/test.desc  [OK] in 0 seconds
>   Running loophead-trace/test-json.desc  [OK] in 0 seconds
>   Running loophead-trace/test-xml.desc  [OK] in 0 seconds
>   Running malloc-may-fail/test.desc  [OK] in 0 seconds
>   Running malloc-may-fail/test_without_option.desc  [OK] in 0 seconds
>   Running malloc-too-large/largest_representable.desc  [OK] in 0 
> seconds
>   Running malloc-too-large/max_size.desc  [OK] in 1 seconds
>   Running malloc-too-large/one_byte_too_large.desc  [OK] in 0 seconds
>   Running member1/test.desc  [OK] in 0 seconds
>   Running member_bounds3/test.desc  [SKIPPED]
>   Running member_bounds4/test.desc  [SKIPPED]
>   Running memory_allocation1/test.desc  [OK] in 0 seconds
>   Running memory_allocation2/test.desc  [OK] in 0 seconds
>   Running memset1/test.desc  [OK] in 0 seconds
>   Running memset2/test.desc  [OK] in 0 seconds
>   Running memset3/test.desc  [OK] in 0 seconds
>   Running memset_null/test.desc  [OK] in 0 seconds
>   Running mm_io1/test.desc  [OK] in 0 seconds
>   Running multiple-goto-traces/test.desc  [OK] in 0 seconds
>   Running nested_label1/test.desc  [OK] in 0 seconds
>   Running no-propagation/test.desc  [OK] in 0 seconds
>   Running no_nondet_static/test.desc  [OK] in 0 seconds
>   Running nondet-pointer/nondet-pointer1.desc  [OK] in 0 seconds
>   Running nondet-pointer/nondet-pointer2.desc  [OK] in 0 seconds
>   Running nondet-pointer/nondet-pointer3.desc  [OK] in 1 seconds
>   Running nondet-pointer/nondet-pointer4.desc  [OK] in 0 seconds
>   Running nondet-pointer/nondet-pointer5.desc  [OK] in 0 seconds
>   Running noop1/test.desc  [OK] in 0 seconds
>   Running noop2/test.desc  [OK] in 0 seconds
>   Running null1/test.desc  [OK] in 0 seconds
>   Running null2/test.desc  [OK] in 0 seconds
>   Running null3/test.desc  [OK] in 0 seconds
>   Running null4/test.desc  [OK] in 0 seconds
>   Running null5/test.desc  [OK] in 0 seconds
>   Running null6/test.desc  [OK] in 0 seconds
>   Running null7/test.desc  [OK] in 0 seconds
>   Running null8/test.desc  [OK] in 0 seconds
>   Running object-bits-parsing/non_numeric.desc  [OK] in 0 seconds
>   Running object-bits-parsing/too_large.desc  [OK] in 0 seconds
>   Running object-bits-parsing/valid.desc  [OK] in 0 seconds
>   Running object-bits-parsing/zero.desc  [OK] in 0 seconds
>   Running offsetof1/test.desc  [OK] in 0 seconds
>   Running overflow/leftshift_overflow-c89.desc  [OK] in 0 seconds
>   Running overflow/leftshift_overflow-c99-full-slice.desc  [OK] in 0 
> seconds
>   Running overflow/leftshift_overflow-c99.desc  [OK] in 0 seconds
>   Running overflow/mod_overflow.desc  [OK] in 0 seconds
>   Running overflow/signed_addition_overflow1.desc  [OK] in 0 seconds
>   Running overflow/signed_addition_overflow2.desc  [OK] in 0 seconds
>   Running overflow/signed_addition_overflow3.desc  [OK] in 0 seconds
>   Running overflow/signed_addition_overflow4.desc  [OK] in 1 seconds
>   Running overflow/signed_multiplication1.desc  [OK] in 0 seconds
>   Running overflow/signed_subtraction1.desc  [OK] in 0 seconds
>   Running overflow/unary_minus_overflow.desc  [OK] in 0 seconds
>   Running path-branch-pointer-call/test.desc  [OK] in 0 seconds
>   Running path-per-path-vccs/test.desc  [OK] in 0 seconds
>   Running phi-merge_uninitialized_values/dynamic.desc  [OK] in 0 
> seconds
>   Running phi-merge_uninitialized_values/global.desc  [OK] in 0 
> seconds
>   Running phi-merge_uninitialized_values/local.desc  [OK] in 0 
> seconds
>   Running phi-merge_uninitialized_values/static_local.desc  [OK] in 
> 0 seconds
>   Running pointer-check-01/test.desc  [OK] in 0 seconds
>   Running pointer-check-02/test.desc  [OK] in 0 seconds
>   Running pointer-extra-checks/test.desc  [OK] in 0 seconds
>   Running pointer-function-parameters/test.desc  [OK] in 0 seconds
>   Running pointer-function-parameters-struct-mutual-recursion/test.desc  
> [OK] in 0 seconds
>   Running pointer-function-parameters-struct-non-recursive/test.desc  
> [OK] in 0 seconds
>   Running pointer-function-parameters-struct-simple-recursion/test.desc  
> [OK] in 0 seconds
>   Running pointer-function-parameters-struct-simple-recursion-2/test.desc  
> [OK] in 1 seconds
>   Running pointer-offset-01/test.desc  [OK] in 0 seconds
>   Running pointer-overflow1/test.desc  [OK] in 0 seconds
>   Running pointer-overflow2/test.desc  [OK] in 0 seconds
>   Running pointer-overflow3/no-simplify.desc  [OK] in 0 seconds
>   Running pointer-overflow3/test.desc  [OK] in 0 seconds
>   Running pointer-overflow4/test.desc  [OK] in 0 seconds
>   Running pointer-predicates/at_bounds1.desc  [OK] in 0 seconds
>   Running pointer-predicates/in_range1.desc  [OK] in 0 seconds
>   Running pointer-primitive-check-01/test.desc  [OK] in 0 seconds
>   Running pointer-primitive-check-02/test.desc  [OK] in 0 seconds
>   Running pointer-primitive-check-04/test.desc  [OK] in 0 seconds
>   Running 
> pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc
>   [OK] in 0 seconds
>   Running points-to-sets/test.desc  [OK] in 0 seconds
>   Running points-to-sets/test_json.desc  [OK] in 0 seconds
>   Running points-to-sets/test_xml.desc  [OK] in 0 seconds
>   Running pragma_cprover1/test.desc  [OK] in 0 seconds
>   Running pragma_cprover2/test.desc  [OK] in 1 seconds
>   Running pragma_cprover3/test.desc  [OK] in 0 seconds
>   Running pragma_cprover_enable1/test.desc  [OK] in 0 seconds
>   Running pragma_cprover_enable2/test.desc  [OK] in 0 seconds
>   Running pragma_cprover_enable3/test.desc  [OK] in 0 seconds
>   Running pragma_cprover_enable_all/test.desc  [OK] in 0 seconds
>   Running pragma_cprover_enable_disable_global_off/test.desc  [OK] 
> in 0 seconds
>   Running pragma_cprover_enable_disable_global_on/test.desc  [OK] in 
> 0 seconds
>   Running pragma_cprover_enable_disable_multiple/test.desc  [OK] in 
> 0 seconds
>   Running printf1/test.desc  [OK] in 0 seconds
>   Running ptr_arithmetic_on_null/test.desc  [OK] in 0 seconds
>   Running ptr_arithmetic_on_null/type_conflict.desc  [OK] in 0 
> seconds
>   Running r_w_ok1/test.desc  [OK] in 0 seconds
>   Running r_w_ok10/test.desc  [OK] in 0 seconds
>   Running r_w_ok2/test.desc  [OK] in 1 seconds
>   Running r_w_ok3/test.desc  [SKIPPED]
>   Running r_w_ok4/test.desc  [OK] in 0 seconds
>   Running r_w_ok5/test.desc  [OK] in 0 seconds
>   Running r_w_ok6/test.desc  [OK] in 0 seconds
>   Running r_w_ok7/test.desc  [OK] in 0 seconds
>   Running r_w_ok8/test.desc  [OK] in 0 seconds
>   Running r_w_ok9/simplify.desc  [OK] in 0 seconds
>   Running r_w_ok9/test.desc  [OK] in 0 seconds
>   Running reachability-slice/test.desc  [OK] in 0 seconds
>   Running reachability-slice/test2.desc  [OK] in 0 seconds
>   Running reachability-slice/test3.desc  [OK] in 0 seconds
>   Running reachability-slice-interproc/test.desc  [OK] in 0 seconds
>   Running reachability-slice-interproc2/test.desc  [OK] in 0 seconds
>   Running reachability-slice-interproc3/test.desc  [OK] in 0 seconds
>   Running realloc-should-not-free-on-failure-to-allocate/test.desc  
> [OK] in 0 seconds
>   Running residual-guards-1/test.desc  [OK] in 0 seconds
>   Running residual-guards-1/test_execution.desc  [OK] in 0 seconds
>   Running residual-guards-2/test.desc  [OK] in 1 seconds
>   Running residual-guards-2/test_execution.desc  [OK] in 0 seconds
>   Running residual-guards-2/unreachable-code.desc  [SKIPPED]
>   Running residual-guards-3/test.desc  [OK] in 0 seconds
>   Running residual-guards-3/test_execution.desc  [OK] in 0 seconds
>   Running residual-guards-4/test.desc  [OK] in 0 seconds
>   Running residual-guards-4/test_execution.desc  [OK] in 0 seconds
>   Running residual-guards-4/unreachable-code.desc  [SKIPPED]
>   Running return1/test.desc  [OK] in 0 seconds
>   Running return2/test.desc  [OK] in 0 seconds
>   Running return3/full-slice.desc  [OK] in 0 seconds
>   Running return3/test.desc  [OK] in 0 seconds
>   Running return4/test.desc  [OK] in 0 seconds
>   Running return5/test.desc  [OK] in 0 seconds
>   Running return6/test.desc  [OK] in 0 seconds
>   Running return7/test.desc  [OK] in 0 seconds
>   Running return8/test.desc  [OK] in 0 seconds
>   Running return9/test.desc  [OK] in 0 seconds
>   Running runtime-profiling/test.desc  [OK] in 0 seconds
>   Running sat-solver/test.desc  [OK] in 1 seconds
>   Running sat-solver-error/test.desc  [OK] in 0 seconds
>   Running sat-solver-warning/test.desc  [OK] in 0 seconds
>   Running saturating_arithmetric/output-formula.desc  [OK] in 0 
> seconds
>   Running saturating_arithmetric/output-goto.desc  [OK] in 0 seconds
>   Running saturating_arithmetric/test.desc  [OK] in 0 seconds
>   Running saturating_arithmetric/typeconflict.desc  [OK] in 0 seconds
>   Running scanf1/big-endian.desc  [OK] in 0 seconds
>   Running scanf1/no-simplify.desc  [SKIPPED]
>   Running scanf1/test.desc  [OK] in 0 seconds
>   Running self_loops_to_assumptions1/default.desc  [OK] in 0 seconds
>   Running self_loops_to_assumptions1/no-assume.desc  [OK] in 0 
> seconds
>   Running set-property-inline1/test.desc  [OK] in 0 seconds
>   Running short_circuit_implies/false_implies_failure_side_effect.desc  
> [OK] in 0 seconds
>   Running short_circuit_implies/short-circuit-memory-checks.desc  
> [OK] in 0 seconds
>   Running short_circuit_implies/true_implies_failure_side_effect.desc  
> [OK] in 0 seconds
>   Running show-vcc/main_prec.desc  [OK] in 0 seconds
>   Running show-vcc/test.desc  [OK] in 0 seconds
>   Running show_properties1/test.desc  [OK] in 0 seconds
>   Running simplify-array-size/test.desc  [OK] in 0 seconds
>   Running simplify-full-test/test.desc  [OK] in 0 seconds
>   Running simplify-function-call-array-element-pointer/test.desc  
> [OK] in 0 seconds
>   Running simplify-function-call-array-pointer/test.desc  [OK] in 0 
> seconds
>   Running simplify-function-call-pointer-access/test.desc  [OK] in 0 
> seconds
>   Running simplify-global-array-access/test.desc  [OK] in 1 seconds
>   Running simplify-local-array-access/test.desc  [OK] in 0 seconds
>   Running simplify-pointer-access/test.desc  [OK] in 0 seconds
>   Running simplify-union/test.desc  [OK] in 0 seconds
>   Running simplify_singleton_interval_7690/negative_test.desc  [OK] 
> in 0 seconds
>   Running simplify_singleton_interval_7690/positive_test.desc  [OK] 
> in 0 seconds
>   Running simplify_singleton_interval_7690/test_smt2.desc  [SKIPPED]
>   Running simplify_singleton_interval_7953/test.desc  [OK] in 0 
> seconds
>   Running stack-trace/test.desc  [OK] in 0 seconds
>   Running string_assignment1/test.desc  [OK] in 0 seconds
>   Running struct1/test.desc  [OK] in 0 seconds
>   Running struct10/test.desc  [OK] in 0 seconds
>   Running struct11/test.desc  [OK] in 0 seconds
>   Running struct12/test.desc  [OK] in 0 seconds
>   Running struct13/test.desc  [OK] in 0 seconds
>   Running struct14/test.desc  [OK] in 0 seconds
>   Running struct15/test.desc  [SKIPPED]
>   Running struct16/test.desc  [OK] in 0 seconds
>   Running struct17/test.desc  [OK] in 0 seconds
>   Running struct3/test.desc  [OK] in 0 seconds
>   Running struct4/test.desc  [OK] in 0 seconds
>   Running struct6/test.desc  [OK] in 0 seconds
>   Running struct7/test.desc  [OK] in 1 seconds
>   Running struct8/test.desc  [OK] in 0 seconds
>   Running struct9/test.desc  [OK] in 0 seconds
>   Running switch1/test.desc  [OK] in 0 seconds
>   Running switch2/test.desc  [OK] in 0 seconds
>   Running switch3/test.desc  [OK] in 0 seconds
>   Running switch4/test.desc  [OK] in 0 seconds
>   Running switch5/test.desc  [OK] in 0 seconds
>   Running switch6/test.desc  [OK] in 0 seconds
>   Running switch7/test.desc  [OK] in 0 seconds
>   Running switch8/program-only.desc  [OK] in 0 seconds
>   Running switch8/test.desc  [OK] in 0 seconds
>   Running switch9/test.desc  [OK] in 0 seconds
>   Running symex_should_evaluate_simple_pointer_conditions/test.desc  
> [OK] in 0 seconds
>   Running symex_should_exclude_null_pointers/nondet.desc  [OK] in 0 
> seconds
>   Running symex_should_exclude_null_pointers/test.desc  [OK] in 0 
> seconds
>   Running symex_should_filter_value_sets/test.desc  [OK] in 0 seconds
>   Running sync_X_and_fetch-1/pointer.desc  [OK] in 0 seconds
>   Running sync_X_and_fetch-1/test.desc  [OK] in 0 seconds
>   Running sync_X_and_fetch-1/two.desc  [OK] in 0 seconds
>   Running sync_bool_compare-1/pointer.desc  [OK] in 0 seconds
>   Running sync_bool_compare-1/test.desc  [OK] in 1 seconds
>   Running sync_bool_compare-1/three.desc  [OK] in 0 seconds
>   Running sync_fetch_and_X-1/pointer.desc  [OK] in 0 seconds
>   Running sync_fetch_and_X-1/test.desc  [OK] in 0 seconds
>   Running sync_fetch_and_X-1/two.desc  [OK] in 0 seconds
>   Running sync_lock_release-1/symbol_per_type.desc  [OK] in 0 seconds
>   Running sync_lock_release-1/test.desc  [OK] in 0 seconds
>   Running sync_val_compare-1/pointer.desc  [OK] in 0 seconds
>   Running sync_val_compare-1/test.desc  [OK] in 0 seconds
>   Running sync_val_compare-1/three.desc  [OK] in 0 seconds
>   Running trace-strings/test.desc  [OK] in 0 seconds
>   Running trace-values/trace-values.desc  [OK] in 0 seconds
>   Running trace-values/unbounded_array.desc  [OK] in 0 seconds
>   Running trace_address_arithmetic1/test.desc  [OK] in 0 seconds
>   Running trace_options_json_extended/extended.desc  [OK] in 0 
> seconds
>   Running trace_options_json_extended/non-extended.desc  [OK] in 0 
> seconds
>   Running trace_show_code/test.desc  [OK] in 0 seconds
>   Running trace_show_function_calls/test.desc  [SKIPPED]
>   Running ts18661_typedefs/test.desc  [OK] in 0 seconds
>   Running typedef-anon-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-anon-struct2/test.desc  [OK] in 0 seconds
>   Running typedef-anon-union1/test.desc  [OK] in 1 seconds
>   Running typedef-anon-union2/test.desc  [OK] in 0 seconds
>   Running typedef-const-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-const-type1/test.desc  [OK] in 0 seconds
>   Running typedef-const-union1/test.desc  [OK] in 0 seconds
>   Running typedef-param-anon-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-param-anon-union1/test.desc  [OK] in 0 seconds
>   Running typedef-param-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-param-type1/test.desc  [OK] in 0 seconds
>   Running typedef-param-type2/test.desc  [OK] in 0 seconds
>   Running typedef-param-type3/test.desc  [OK] in 0 seconds
>   Running typedef-param-union1/test.desc  [OK] in 0 seconds
>   Running typedef-return-anon-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-return-anon-union1/test.desc  [OK] in 0 seconds
>   Running typedef-return-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-return-type1/test.desc  [OK] in 0 seconds
>   Running typedef-return-type2/test.desc  [OK] in 0 seconds
>   Running typedef-return-type3/test.desc  [OK] in 0 seconds
>   Running typedef-return-union1/test.desc  [OK] in 0 seconds
>   Running typedef-struct1/test.desc  [OK] in 0 seconds
>   Running typedef-struct2/test.desc  [OK] in 0 seconds
>   Running typedef-type1/test.desc  [OK] in 0 seconds
>   Running typedef-type2/test.desc  [OK] in 0 seconds
>   Running typedef-type3/test.desc  [OK] in 0 seconds
>   Running typedef-type4/test.desc  [OK] in 0 seconds
>   Running typedef-union1/test.desc  [OK] in 0 seconds
>   Running typedef-union2/test.desc  [OK] in 0 seconds
>   Running uncaught_exceptions_analysis1/test.desc  [OK] in 1 seconds
>   Running uniform_array1/test.desc  [OK] in 0 seconds
>   Running uninterpreted_function/uf1.desc  [OK] in 0 seconds
>   Running uninterpreted_function/uf2.desc  [OK] in 0 seconds
>   Running union/union_initialization.desc  [OK] in 0 seconds
>   Running union/union_large_array.desc  [OK] in 0 seconds
>   Running union/union_member.desc  [OK] in 0 seconds
>   Running union/union_update.desc  [OK] in 0 seconds
>   Running union-unequal-element-size1/test.desc  [OK] in 0 seconds
>   Running union1/test.desc  [OK] in 0 seconds
>   Running union10/union_list2.desc  [OK] in 1 seconds
>   Running union11/union_list.desc  [OK] in 0 seconds
>   Running union12/test.desc  [OK] in 0 seconds
>   Running union13/no-arch.desc  [OK] in 0 seconds
>   Running union13/test.desc  [OK] in 0 seconds
>   Running union14/test.desc  [OK] in 0 seconds
>   Running union15/test.desc  [OK] in 0 seconds
>   Running union16/test.desc  [OK] in 0 seconds
>   Running union17/test.desc  [OK] in 0 seconds
>   Running union18/test.desc  [OK] in 0 seconds
>   Running union2/test.desc  [OK] in 0 seconds
>   Running union3/test.desc  [OK] in 0 seconds
>   Running union4/test.desc  [OK] in 0 seconds
>   Running union5/test.desc  [OK] in 0 seconds
>   Running union6/test.desc  [OK] in 0 seconds
>   Running union7/test.desc  [OK] in 0 seconds
>   Running union8/test.desc  [OK] in 0 seconds
>   Running union9/test.desc  [OK] in 0 seconds
>   Running unknown-argument-suggestion/test.desc  [OK] in 0 seconds
>   Running unreachable-goto1/test-vccs.desc  [OK] in 0 seconds
>   Running unreachable-goto1/test.desc  [OK] in 0 seconds
>   Running unreachable-goto2/test-vccs.desc  [OK] in 0 seconds
>   Running unreachable-goto2/test.desc  [OK] in 0 seconds
>   Running unreachable-goto3/test-vccs.desc  [OK] in 1 seconds
>   Running unreachable-goto3/test.desc  [OK] in 0 seconds
>   Running unreachable-goto4/test-vccs.desc  [OK] in 0 seconds
>   Running unreachable-goto4/test.desc  [OK] in 0 seconds
>   Running unreachable-goto5/test-vccs.desc  [OK] in 0 seconds
>   Running unreachable-goto5/test.desc  [OK] in 0 seconds
>   Running unreachable-goto6/test-vccs.desc  [OK] in 0 seconds
>   Running unreachable-goto6/test.desc  [OK] in 0 seconds
>   Running unsigned1/test.desc  [OK] in 0 seconds
>   Running unsigned___int128/test.desc  [OK] in 0 seconds
>   Running unsigned_char1/test.desc  [OK] in 0 seconds
>   Running unwind_counters1/test.desc  [OK] in 0 seconds
>   Running unwind_counters2/test.desc  [OK] in 0 seconds
>   Running unwind_counters3/test.desc  [OK] in 0 seconds
>   Running unwind_counters4/test.desc  [OK] in 0 seconds
>   Running unwinding_assertions1/test.desc  [OK] in 0 seconds
>   Running unwindset1/label.desc  [OK] in 0 seconds
>   Running unwindset1/test.desc  [OK] in 0 seconds
>   Running unwindset2/test.desc  [OK] in 0 seconds
>   Running va_list1/test.desc  [OK] in 0 seconds
>   Running va_list2/test.desc  [OK] in 0 seconds
>   Running va_list3/test.desc  [OK] in 0 seconds
>   Running va_list3/windows-preprocessed.desc  [OK] in 1 seconds
>   Running va_list4/test.desc  [OK] in 0 seconds
>   Running variable-access-to-constant-array/test.desc  [OK] in 0 
> seconds
>   Running verifier_assume_lhs/test.desc  [SKIPPED]
>   Running verifier_assume_one/test.desc  [OK] in 0 seconds
>   Running verifier_error_lhs/test.desc  [OK] in 0 seconds
>   Running verifier_error_zero/test.desc  [OK] in 0 seconds
>   Running vla1/program-only.desc  [OK] in 0 seconds
>   Running vla1/test.desc  [OK] in 0 seconds
>   Running vla2/test.desc  [SKIPPED]
>   Running vla3/test.desc  [SKIPPED]
>   Running void_ifthenelse/test.desc  [OK] in 0 seconds
>   Running void_pointer1/test.desc  [OK] in 0 seconds
>   Running void_pointer2/test.desc  [OK] in 0 seconds
>   Running void_pointer3/test.desc  [OK] in 0 seconds
>   Running void_pointer4/test.desc  [OK] in 0 seconds
>   Running void_pointer5/test.desc  [OK] in 0 seconds
>   Running void_pointer6/test.desc  [OK] in 0 seconds
>   Running void_pointer7/test.desc  [OK] in 0 seconds
>   Running while1/test.desc  [OK] in 0 seconds
>   Running while2/requires-transform.desc  [OK] in 0 seconds
>   Running while2/test.desc  [OK] in 0 seconds
>   Running xml-escaping/debug_output.desc  [OK] in 0 seconds
>   Running xml-interface1/test.desc  [OK] in 0 seconds
>   Running xml-interface1/test_wrong_flag.desc  [OK] in 0 seconds
>   Running xml-interface1/test_wrong_option.desc  [OK] in 0 seconds
>   Running xml-trace/test.desc  [OK] in 0 seconds
>   Running xml-trace2/test.desc  [OK] 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]
> 
> Tests failed
>   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.

--- End Message ---

--- Begin Message ---

Source: cbmc
Source-Version: 5.95.1-5
Done: Michael Tautschnig <m...@debian.org>

We believe that the bug you reported is fixed in the latest version of
cbmc, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1069...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Michael Tautschnig <m...@debian.org> (supplier of updated cbmc package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmas...@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Format: 1.8
Date: Mon, 29 Apr 2024 12:56:13 +0000
Source: cbmc
Binary: cbmc cbmc-dbgsym jbmc jbmc-dbgsym
Architecture: source
Version: 5.95.1-5
Distribution: unstable
Urgency: low
Maintainer: Michael Tautschnig <m...@debian.org>
Changed-By: Michael Tautschnig <m...@debian.org>
Description:
 cbmc       - bounded model checker for C and C++ programs
 jbmc       - bounded model checker for Java programs
Closes: 1069438 1069990
Changes:
 cbmc (5.95.1-5) unstable; urgency=low
 .
   * Add fopen64 support (Closes: #1069438)
   * Add loong64 support - thanks wuruilong for the patch (Closes: #1069990)
Checksums-Sha1:
 ef9efca463b99f79ca1c0cbacfdb04a732cf2bf2 3061 cbmc_5.95.1-5.dsc
 0c39a83a339b5f2fa27e39f6cc43a5363b22b1a2 16944 cbmc_5.95.1-5.debian.tar.xz
Checksums-Sha256:
 59d0d9a22a86db411c0cdb0eceb3ede4e059e3d9741fad68015329dbb6354809 3061 
cbmc_5.95.1-5.dsc
 eb865cf8bbdf528a73a6cd6f6bd4885e185405a56885e2d71158273fb233a74c 16944 
cbmc_5.95.1-5.debian.tar.xz
Files:
 162b93dd6b16da530cc9b51e21b7ba7b 3061 science optional cbmc_5.95.1-5.dsc
 e4b045e334cc786d094c2658a4917ac4 16944 science optional 
cbmc_5.95.1-5.debian.tar.xz

-----BEGIN PGP SIGNATURE-----

iQJCBAEBCgAsFiEErKbD9OEAOYbzU4gEO7+DkzbsqTEFAmYvpKIOHG10QGRlYmlh
bi5vcmcACgkQO7+DkzbsqTHapA/+Ny6iYfqEYtAwe79d22Xh7D88kAXZzdDaYScv
6LxzE+1xggprVUHgcCNxBPgnmw+4AVydMs6ekuSMtKOjtvYFmBHN3CRhCU5Xf2Qs
efdXqdnUS1ru5ekr7GLCkMgZ7hoo2LFymGwaWI85Rr1wvCYGqzuLSNGEXr8huQ7d
J1kH6agvAuI+qW7R4rCsJcIV5S662PaOsFI+Rq5bdemvTCiyMqi5p4VIGNYqu1XI
dfgB+t0Fsbj4FJoy7J09k97lzwRRCt8IdudJVCS9DQ+TsuRF2g7FR7vdGN1gvZN5
wGDmnerk6IVat9XQ0aGGSvj9yk8JNhJjbiZtxFq+hRoKEQ21XvDySvj4aqVezYh1
C1aEQ6Ccf/Ynip9wR4MNbWDrYU/zpT3xE70qMWHd4iZhMGrFy9OuKjaZqzy08JET
G6TysI7744CGLVLKZLmthZ0syvDRuDUCu1/mhjXO7ZTBxejYJ7148ejixdYuOyxP
De5P4mF3pqUAbs3tH+o0EDQZflCGcPXf7QMSSZPwSdvpS8wSRctqqSlWboxlpJ65
uCIqTtGombzhVvVywbGqfgQeGSx796QZxjhNrFo2M/1XPTSRoIo7h/HsouCf5DRf
QVgKlHchDIAH9hBHxg7UkGhw9w6ODA8JyTRcjPDsGc0goikC/SVi0Z7sGlMlPy0H
P7ZZ6gA=
=X4Wi
-----END PGP SIGNATURE-----

pgpmoMxY4Ok8L.pgp
Description: PGP signature

--- End Message ---