BENCHMARK INFORMATION benchmark definition: ../../benchmark-defs/full-runs/ultimateunihorn.xml name: ultimateunihorn run sets: CHC-COMP2025_check-sat.LIA-Lin-Arrays date: Mon, 2025-05-05 20:07:07 CEST tool: Ultimate Unihorn (unknown version) tool executable: ./chc-comp-wrapper.sh options: resource limits: - memory: 30000.0 MB - time: 1800 s - cpu cores: 8 hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz - cpu cores: 8 - memory: 30000.0 MB ------------------------------------------------------------ CHC-COMP2025_check-sat.LIA-Lin-Arrays Run set 1 of 1 with options '' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- quic3/data/array_monotonic_true-unreach-call_000.smt2 unknown 9.87 2.69 apollon095 quic3/data/standard_palindrome_true-unreach-call_ground_000.smt2 unknown 9.84 2.57 apollon067 quic3/data/standard_copy7_true-unreach-call_ground_000.smt2 TIMEOUT 1800.81 1628.31 apollon039 quic3/data/standard_init3_true-unreach-call_ground_000.smt2 unknown 9.24 2.39 apollon004 quic3/data/array_init_const_000.smt2 unknown 9.36 2.43 apollon004 quic3/data/sanfoundry_10_true-unreach-call_ground_000.smt2 unknown 9.66 2.51 apollon028 quic3/data/standard_partition_original_true-unreach-call_ground_000.smt2 TIMEOUT 1800.35 1713.54 apollon058 quic3/data/standard_copy5_true-unreach-call_ground_000.smt2 unknown 10.35 2.66 apollon117 quic3/data/standard_init5_true-unreach-call_ground_000.smt2 unknown 9.38 2.41 apollon098 quic3/data/array_mul_init_true-unreach-call_1_000.smt2 TIMEOUT 1800.77 1649.39 apollon019 quic3/data/sanfoundry_27_true-unreach-call_ground_000.smt2 unknown 9.84 2.57 apollon040 quic3/data/standard_copy3_true-unreach-call_ground_000.smt2 unknown 9.16 2.46 apollon048 quic3/data/standard_partition_true-unreach-call_ground_000.smt2 unknown 9.52 2.49 apollon141 quic3/data/standard_copy1_true-unreach-call_ground_000.smt2 unknown 9.37 2.46 apollon021 quic3/data/array_reverse_000.smt2 unknown 1642.59 1359.62 apollon062 quic3/data/array_nd_two_times_cell_true_000.smt2 unknown 9.37 2.46 apollon028 quic3/data/standard_init8_true-unreach-call_ground_000.smt2 unknown 9.75 2.57 apollon155 quic3/data/standard_sort_N_nd_assert_loop_000.smt2 TIMEOUT 1800.49 1717.29 apollon027 quic3/data/standard_copy4_true-unreach-call_ground_000.smt2 TIMEOUT 1801.20 1690.78 apollon100 quic3/data/standard_copy8_true-unreach-call_ground_000.smt2 unknown 10.18 2.89 apollon144 quic3/data/standard_copyInitSum_true-unreach-call_ground_000.smt2 unknown 9.69 2.52 apollon141 quic3/data/array_monotonic_set_000.smt2 TIMEOUT 1800.54 1629.48 apollon040 quic3/data/standard_init2_true-unreach-call_ground_000.smt2 unknown 9.37 2.44 apollon028 quic3/data/standard_compareModified_true-unreach-call_ground_000.smt2 unknown 9.70 2.44 apollon058 quic3/data/standard_maxInArray_true-unreach-call_ground_000.smt2 TIMEOUT 1801.05 1646.79 apollon044 quic3/data/standard_init6_true-unreach-call_ground_000.smt2 unknown 10.40 2.85 apollon062 quic3/data/standard_vector_difference_true-unreach-call_ground_000.smt2 TIMEOUT 1800.62 1609.36 apollon118 quic3/data/standard_copy2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.38 1683.38 apollon130 quic3/data/standard_copyInitSum3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.94 1675.56 apollon146 quic3/data/standard_copy6_true-unreach-call_ground_000.smt2 TIMEOUT 1801.21 1686.34 apollon080 quic3/data/standard_find_true-unreach-call_ground_000.smt2 TIMEOUT 1800.62 1544.88 apollon021 quic3/data/standard_vararg_true-unreach-call_ground_true-termination_000.smt2 unknown 9.57 2.85 apollon104 quic3/data/array_init_partial_000.smt2 unknown 9.59 2.52 apollon082 quic3/data/standard_copyInit_true-unreach-call_ground_000.smt2 unknown 10.11 2.96 apollon122 quic3/data/standard_minInArray_true-unreach-call_ground_000.smt2 TIMEOUT 1800.80 1643.21 apollon075 quic3/data/standard_copyInitSum2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.80 1632.12 apollon145 quic3/data/standard_copy9_true-unreach-call_ground_000.smt2 TIMEOUT 1800.93 1653.88 apollon141 quic3/data/standard_init9_true-unreach-call_ground_000.smt2 unknown 9.59 2.46 apollon118 quic3/data/standard_init4_true-unreach-call_ground_000.smt2 unknown 9.49 2.50 apollon145 quic3/data/standard_init7_true-unreach-call_ground_000.smt2 unknown 9.40 2.45 apollon125 quic3/data/array_swap_twice_000.smt2 TIMEOUT 1801.18 1726.77 apollon122 quic3/data/sanfoundry_02_true-unreach-call_ground_000.smt2 unknown 9.95 2.55 apollon062 quic3/data/array_swap_000.smt2 unknown 598.09 544.48 apollon074 hcai-bench/svcomp/O3/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 true 12.43 3.66 apollon166 hcai-bench/svcomp/O3/eureka_01_false-unreach-call_000.smt2 unknown 9.76 2.49 apollon028 hcai-bench/svcomp/O3/linear_sea.ch_true-unreach-call_000.smt2 false 11.59 3.27 apollon117 hcai-bench/svcomp/O3/eureka_01_true-unreach-call_000.smt2 TIMEOUT 1801.28 1577.53 apollon125 hcai-bench/svcomp/O3/n.c40_true-unreach-call_true-termination_000.smt2 true 10.88 3.09 apollon152 hcai-bench/svcomp/O3/vogal_false-unreach-call_000.smt2 unknown 9.84 2.56 apollon082 hcai-bench/svcomp/O3/ludcmp_false-unreach-call_000.smt2 false 13.84 3.66 apollon044 hcai-bench/svcomp/O3/linear_search_false-unreach-call_000.smt2 false 11.25 3.24 apollon028 hcai-bench/svcomp/O3/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination_000.smt2 unknown 9.84 2.60 apollon082 hcai-bench/svcomp/O3/matrix_false-unreach-call_true-termination_000.smt2 false 13.93 3.74 apollon048 hcai-bench/svcomp/O3/invert_string_true-unreach-call_true-termination_000.smt2 unknown 10.15 2.53 apollon028 hcai-bench/svcomp/O3/while_infinite_loop_4_false-unreach-call_true-termination_000.smt2 false 10.86 3.44 apollon023 hcai-bench/svcomp/O3/insertion_sort_false-unreach-call_true-termination_000.smt2 unknown 10.29 2.74 apollon125 hcai-bench/svcomp/O3/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination_000.smt2 unknown 10.66 3.03 apollon145 hcai-bench/svcomp/O3/sum_array_false-unreach-call_000.smt2 unknown 10.35 2.77 apollon067 hcai-bench/svcomp/O3/invert_string_false-unreach-call_true-termination_000.smt2 unknown 9.52 2.41 apollon004 hcai-bench/svcomp/O3/string_true-unreach-call_true-termination_000.smt2 unknown 9.50 2.49 apollon146 hcai-bench/svcomp/O3/insertion_sort_true-unreach-call_true-termination_000.smt2 unknown 10.11 2.61 apollon126 hcai-bench/svcomp/O3/lu.cmp_true-unreach-call_000.smt2 true 12.50 3.32 apollon075 hcai-bench/svcomp/O3/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination_000.smt2 unknown 9.87 2.53 apollon021 hcai-bench/svcomp/O3/trex02_true-unreach-call_true-termination_000.smt2 unknown 9.58 2.43 apollon144 hcai-bench/svcomp/O3/string_false-unreach-call_true-termination_000.smt2 false 13.25 3.56 apollon058 hcai-bench/svcomp/O3/verisec_NetBSD-libc__loop_false-unreach-call_true-termination_000.smt2 false 11.68 3.26 apollon144 hcai-bench/svcomp/O3/nec40_true-unreach-call_true-termination_000.smt2 true 10.89 2.98 apollon074 hcai-bench/svcomp/O3/vogal_true-unreach-call_000.smt2 true 478.67 413.41 apollon068 hcai-bench/svcomp/O3/eureka_05_true-unreach-call_true-termination_000.smt2 true 34.86 11.27 apollon052 hcai-bench/svcomp/O3/sum_array_true-unreach-call_000.smt2 unknown 9.58 2.49 apollon023 hcai-bench/svcomp/O3/compact_false-unreach-call_000.smt2 unknown 10.26 2.79 apollon040 hcai-bench/svcomp/O3/trex02_false-unreach-call_true-termination_000.smt2 unknown 9.79 2.52 apollon023 hcai-bench/svcomp/O0/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 hcai-bench/svcomp/O0/n.c40_true-unreach-call_true-termination_000.smt2 hcai-bench/svcomp/O0/vogal_false-unreach-call_000.smt2 hcai-bench/svcomp/O0/array_true-unreach-call_true-termination_000.smt2 unknown 9.51 2.55 apollon086 hcai-bench/svcomp/O0/matrix_true-unreach-call_true-termination_000.smt2 unknown 9.36 2.39 apollon021 hcai-bench/svcomp/O0/array_false-unreach-call_true-termination_000.smt2 unknown 9.43 2.46 apollon082 hcai-bench/svcomp/O0/string_true-unreach-call_true-termination_000.smt2 hcai-bench/svcomp/O0/string_false-unreach-call_true-termination_000.smt2 hcai-bench/svcomp/O0/vogal_true-unreach-call_000.smt2 hcai-bench/svcomp/O0/compact_false-unreach-call_000.smt2 llreve-bench/smt2/arrays/libc__memchr_1.array_000.smt2 true 51.16 23.62 apollon048 llreve-bench/smt2/arrays/libc__stpcpy_1.array_000.smt2 true 40.11 17.16 apollon098 llreve-bench/smt2/arrays/coreutils__md5sum.array_000.smt2 unknown 9.77 2.55 apollon052 llreve-bench/smt2/arrays/libc__strpbrk_2.array_000.smt2 unknown 9.28 2.42 apollon166 llreve-bench/smt2/arrays/heap__memcpy_a.array_000.smt2 true 37.49 15.33 apollon126 llreve-bench/smt2/arrays/heap__fib.array_000.smt2 unknown 9.83 2.57 apollon082 llreve-bench/smt2/arrays/heap__memcpy_b.array_000.smt2 unknown 9.54 2.44 apollon166 llreve-bench/smt2/arrays/heap__propagate.array_000.smt2 unknown 9.80 2.63 apollon092 llreve-bench/smt2/arrays/heap__findmax.array_000.smt2 true 96.61 59.30 apollon016 llreve-bench/smt2/arrays/libc__memset_1.array_000.smt2 true 22.87 7.58 apollon152 llreve-bench/smt2/arrays/libc__strncmp_1.array_000.smt2 true 88.98 49.65 apollon023 llreve-bench/smt2/arrays/libc__memmove_1.array_000.smt2 true 35.96 11.53 apollon142 llreve-bench/smt2/arrays/heap__clearstr.array_000.smt2 true 49.02 18.44 apollon079 llreve-bench/smt2/arrays/libc__memccpy_1.array_000.smt2 unknown 9.46 2.54 apollon033 llreve-bench/smt2/arrays/libc__strcspn.array_000.smt2 true 118.17 75.53 apollon033 llreve-bench/smt2/arrays/heap__selsort.array_000.smt2 TIMEOUT 1800.69 1731.74 apollon052 llreve-bench/smt2/arrays/libc__strcmp.array_000.smt2 unknown 9.89 2.60 apollon146 llreve-bench/smt2/arrays/libc__strpbrk_1.array_000.smt2 true 86.98 48.89 apollon150 llreve-bench/smt2/arrays/heap__cocome2.array_000.smt2 true 59.91 28.96 apollon130 llreve-bench/smt2/arrays/libc__strchr_1.array_000.smt2 true 289.08 237.85 apollon048 llreve-bench/smt2/arrays/libc__strncmp_3.array_000.smt2 true 58.40 27.74 apollon133 llreve-bench/smt2/arrays/libc__memrchr_1.array_000.smt2 true 41.24 15.69 apollon028 llreve-bench/smt2/arrays/libc__strncmp_2.array_000.smt2 true 58.17 25.60 apollon139 llreve-bench/smt2/arrays/libc__strpbrk_3.array_000.smt2 unknown 8.85 2.36 apollon142 llreve-bench/muz/heap__memcpy_b_000.smt2 true 87.56 60.83 apollon095 llreve-bench/muz/heap__propagate_000.smt2 true 38.17 15.58 apollon040 llreve-bench/muz/heap__findmax_000.smt2 true 102.85 64.67 apollon067 llreve-bench/muz/libc__memccpy_1_000.smt2 unknown 9.53 2.44 apollon146 llreve-bench/muz/libc__stpcpy_1_000.smt2 true 42.14 18.10 apollon082 llreve-bench/muz/libc__memset_1_000.smt2 true 23.13 7.66 apollon141 llreve-bench/muz/libc__memmove_1_000.smt2 true 41.94 15.84 apollon079 llreve-bench/muz/heap__clearstr_000.smt2 true 42.90 18.70 apollon098 llreve-bench/muz/heap__memcpy_a_000.smt2 true 38.88 17.85 apollon045 llreve-bench/muz/libc__strcspn_3_000.smt2 false 11.09 3.07 apollon133 llreve-bench/muz/libc__strncmp_2_000.smt2 true 65.98 33.07 apollon043 llreve-bench/muz/heap__heap_call_000.smt2 true 12.66 3.38 apollon139 llreve-bench/muz/libc__memrchr_1_000.smt2 unknown 9.20 2.39 apollon058 llreve-bench/muz/libc__strcmp_000.smt2 true 41.59 15.93 apollon075 llreve-bench/muz/libc__memchr_1_000.smt2 unknown 9.87 3.02 apollon043 llreve-bench/muz/heap__cocome2_000.smt2 true 49.04 21.37 apollon166 llreve-bench/muz/libc__strcspn_000.smt2 true 100.98 60.33 apollon092 llreve-bench/muz/heap__swaparray_000.smt2 false 10.83 3.20 apollon062 llreve-bench/muz/libc__strpbrk_1_000.smt2 true 103.93 63.31 apollon129 llreve-bench/muz/libc__strncmp_1_000.smt2 true 66.29 32.63 apollon045 llreve-bench/muz/coreutils__remove_000.smt2 false 12.93 3.52 apollon117 llreve-bench/muz/libc__sbrk_1_000.smt2 unknown 10.09 2.60 apollon166 llreve-bench/muz/heap__fib_000.smt2 true 53.03 25.03 apollon086 llreve-bench/muz/libc__strncmp_3_000.smt2 true 59.26 28.15 apollon104 llreve-bench/muz/libc__strpbrk_3_000.smt2 true 95.85 56.74 apollon103 llreve-bench/muz/libc__strchr_1_000.smt2 true 221.34 172.01 apollon152 llreve-bench/muz/libc__memmem_1_000.smt2 unknown 10.04 2.93 apollon045 llreve-bench/muz/heap__selsort_000.smt2 unknown 9.36 2.43 apollon039 llreve-bench/muz/coreutils__md5sum_000.smt2 true 1681.79 1567.11 apollon167 llreve-bench/muz/libc__strpbrk_2_000.smt2 true 80.72 45.67 apollon004 llreve-bench/muz/libc__strcspn_2_000.smt2 false 10.91 3.18 apollon016 llreve-bench/unsolved/arrayOffByOne_000.smt2 unknown 9.42 2.48 apollon044 llreve-bench/unsolved/shiftByOne_000.smt2 unknown 9.85 2.53 apollon044 ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 3528.39 - Statistics: 132 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 79