BENCHMARK INFORMATION benchmark definition: ../../benchmark-defs/full-runs/theta.xml name: theta run sets: CHC-COMP2025_check-sat.LIA-Lin-Arrays date: Tue, 2025-05-06 14:29:52 CEST tool: ThetaCHC 6.13.2 tool executable: ./chc 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 TIMEOUT 1800.53 1793.46 apollon054 quic3/data/standard_palindrome_true-unreach-call_ground_000.smt2 TIMEOUT 1800.56 1793.68 apollon020 quic3/data/standard_copy7_true-unreach-call_ground_000.smt2 TIMEOUT 1800.63 1789.41 apollon097 quic3/data/standard_init3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.59 1792.81 apollon018 quic3/data/array_init_const_000.smt2 TIMEOUT 1800.56 1794.22 apollon105 quic3/data/sanfoundry_10_true-unreach-call_ground_000.smt2 TIMEOUT 1800.58 1792.65 apollon108 quic3/data/standard_partition_original_true-unreach-call_ground_000.smt2 TIMEOUT 1800.52 1794.58 apollon161 quic3/data/standard_copy5_true-unreach-call_ground_000.smt2 TIMEOUT 1800.61 1790.99 apollon088 quic3/data/standard_init5_true-unreach-call_ground_000.smt2 TIMEOUT 1800.60 1792.11 apollon010 quic3/data/array_mul_init_true-unreach-call_1_000.smt2 TIMEOUT 1800.53 1793.98 apollon022 quic3/data/sanfoundry_27_true-unreach-call_ground_000.smt2 TIMEOUT 1800.58 1793.86 apollon080 quic3/data/standard_copy3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.59 1792.39 apollon092 quic3/data/standard_partition_true-unreach-call_ground_000.smt2 TIMEOUT 1800.55 1793.22 apollon012 quic3/data/standard_copy1_true-unreach-call_ground_000.smt2 TIMEOUT 1800.56 1793.59 apollon025 quic3/data/array_reverse_000.smt2 TIMEOUT 1800.57 1792.38 apollon042 quic3/data/array_nd_two_times_cell_true_000.smt2 TIMEOUT 1800.51 1794.76 apollon139 quic3/data/standard_init8_true-unreach-call_ground_000.smt2 TIMEOUT 1800.60 1790.59 apollon043 quic3/data/standard_sort_N_nd_assert_loop_000.smt2 TIMEOUT 1800.57 1794.45 apollon005 quic3/data/standard_copy4_true-unreach-call_ground_000.smt2 TIMEOUT 1800.58 1791.90 apollon045 quic3/data/standard_copy8_true-unreach-call_ground_000.smt2 TIMEOUT 1800.63 1788.67 apollon114 quic3/data/standard_copyInitSum_true-unreach-call_ground_000.smt2 TIMEOUT 1800.57 1793.37 apollon142 quic3/data/array_monotonic_set_000.smt2 TIMEOUT 1800.52 1793.48 apollon136 quic3/data/standard_init2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.58 1793.37 apollon052 quic3/data/standard_compareModified_true-unreach-call_ground_000.smt2 TIMEOUT 1800.59 1791.97 apollon115 quic3/data/standard_maxInArray_true-unreach-call_ground_000.smt2 TIMEOUT 1800.57 1794.08 apollon027 quic3/data/standard_init6_true-unreach-call_ground_000.smt2 TIMEOUT 1800.60 1791.95 apollon023 quic3/data/standard_vector_difference_true-unreach-call_ground_000.smt2 TIMEOUT 1800.56 1793.46 apollon008 quic3/data/standard_copy2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.56 1793.14 apollon025 quic3/data/standard_copyInitSum3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.72 1793.01 apollon013 quic3/data/standard_copy6_true-unreach-call_ground_000.smt2 TIMEOUT 1800.63 1789.61 apollon137 quic3/data/standard_find_true-unreach-call_ground_000.smt2 TIMEOUT 1800.57 1793.74 apollon107 quic3/data/standard_vararg_true-unreach-call_ground_true-termination_000.smt2 TIMEOUT 1800.55 1794.01 apollon086 quic3/data/array_init_partial_000.smt2 TIMEOUT 1800.60 1794.03 apollon117 quic3/data/standard_copyInit_true-unreach-call_ground_000.smt2 TIMEOUT 1800.58 1793.07 apollon162 quic3/data/standard_minInArray_true-unreach-call_ground_000.smt2 TIMEOUT 1800.56 1793.60 apollon151 quic3/data/standard_copyInitSum2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.59 1793.06 apollon165 quic3/data/standard_copy9_true-unreach-call_ground_000.smt2 TIMEOUT 1800.84 1788.22 apollon123 quic3/data/standard_init9_true-unreach-call_ground_000.smt2 TIMEOUT 1800.61 1791.20 apollon006 quic3/data/standard_init4_true-unreach-call_ground_000.smt2 TIMEOUT 1800.58 1792.75 apollon050 quic3/data/standard_init7_true-unreach-call_ground_000.smt2 TIMEOUT 1800.61 1790.54 apollon121 quic3/data/array_swap_twice_000.smt2 TIMEOUT 1800.60 1791.04 apollon070 quic3/data/sanfoundry_02_true-unreach-call_ground_000.smt2 TIMEOUT 1800.60 1791.83 apollon091 quic3/data/array_swap_000.smt2 TIMEOUT 1800.59 1793.32 apollon016 hcai-bench/svcomp/O3/O3_veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 true 7.37 2.86 apollon025 hcai-bench/svcomp/O3/O3_eureka_01_false-unreach-call_000.smt2 unknown 31.44 22.38 apollon070 hcai-bench/svcomp/O3/O3_linear_sea.ch_true-unreach-call_000.smt2 unknown 4.74 1.85 apollon136 hcai-bench/svcomp/O3/O3_eureka_01_true-unreach-call_000.smt2 TIMEOUT 1800.57 1790.88 apollon125 hcai-bench/svcomp/O3/O3_n.c40_true-unreach-call_true-termination_000.smt2 true 2.78 1.04 apollon090 hcai-bench/svcomp/O3/O3_vogal_false-unreach-call_000.smt2 unknown 15.04 7.84 apollon052 hcai-bench/svcomp/O3/O3_ludcmp_false-unreach-call_000.smt2 true 6.29 1.94 apollon026 hcai-bench/svcomp/O3/O3_linear_search_false-unreach-call_000.smt2 unknown 4.38 1.74 apollon091 hcai-bench/svcomp/O3/O3_veris.c_NetBSD-libc__loop_true-unreach-call_true-termination_000.smt2 true 4.63 1.57 apollon123 hcai-bench/svcomp/O3/O3_matrix_false-unreach-call_true-termination_000.smt2 false 6.28 1.96 apollon059 hcai-bench/svcomp/O3/O3_invert_string_true-unreach-call_true-termination_000.smt2 true 6.45 1.89 apollon026 hcai-bench/svcomp/O3/O3_while_infinite_loop_4_false-unreach-call_true-termination_000.smt2 unknown 3.64 1.53 apollon030 hcai-bench/svcomp/O3/O3_insertion_sort_false-unreach-call_true-termination_000.smt2 true 7.45 2.11 apollon086 hcai-bench/svcomp/O3/O3_veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination_000.smt2 true 122.36 114.85 apollon094 hcai-bench/svcomp/O3/O3_sum_array_false-unreach-call_000.smt2 false 10.05 3.20 apollon099 hcai-bench/svcomp/O3/O3_invert_string_false-unreach-call_true-termination_000.smt2 false 9.81 3.71 apollon032 hcai-bench/svcomp/O3/O3_string_true-unreach-call_true-termination_000.smt2 true 31.54 25.72 apollon094 hcai-bench/svcomp/O3/O3_insertion_sort_true-unreach-call_true-termination_000.smt2 true 7.69 2.06 apollon026 hcai-bench/svcomp/O3/O3_lu.cmp_true-unreach-call_000.smt2 true 6.93 1.97 apollon107 hcai-bench/svcomp/O3/O3_verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination_000.smt2 unknown 12.96 5.58 apollon003 hcai-bench/svcomp/O3/O3_trex02_true-unreach-call_true-termination_000.smt2 TIMEOUT 1800.60 1792.60 apollon004 hcai-bench/svcomp/O3/O3_string_false-unreach-call_true-termination_000.smt2 unknown 9.87 3.79 apollon114 hcai-bench/svcomp/O3/O3_verisec_NetBSD-libc__loop_false-unreach-call_true-termination_000.smt2 false 4.09 1.50 apollon136 hcai-bench/svcomp/O3/O3_nec40_true-unreach-call_true-termination_000.smt2 true 2.87 1.26 apollon004 hcai-bench/svcomp/O3/O3_vogal_true-unreach-call_000.smt2 true 12.14 6.58 apollon070 hcai-bench/svcomp/O3/O3_eureka_05_true-unreach-call_true-termination_000.smt2 true 8.12 2.62 apollon032 hcai-bench/svcomp/O3/O3_sum_array_true-unreach-call_000.smt2 TIMEOUT 1800.63 1788.97 apollon159 hcai-bench/svcomp/O3/O3_compact_false-unreach-call_000.smt2 TIMEOUT 1800.53 1793.62 apollon055 hcai-bench/svcomp/O3/O3_trex02_false-unreach-call_true-termination_000.smt2 unknown 4.27 1.58 apollon094 hcai-bench/svcomp/O0/O0_veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 true 9.03 4.15 apollon115 hcai-bench/svcomp/O0/O0_n.c40_true-unreach-call_true-termination_000.smt2 TIMEOUT 1800.56 1793.79 apollon140 hcai-bench/svcomp/O0/O0_vogal_false-unreach-call_000.smt2 unknown 690.56 681.55 apollon062 hcai-bench/svcomp/O0/O0_array_true-unreach-call_true-termination_000.smt2 true 4.12 1.52 apollon020 hcai-bench/svcomp/O0/O0_matrix_true-unreach-call_true-termination_000.smt2 true 4.41 1.48 apollon070 hcai-bench/svcomp/O0/O0_array_false-unreach-call_true-termination_000.smt2 unknown 4.86 1.65 apollon026 hcai-bench/svcomp/O0/O0_string_true-unreach-call_true-termination_000.smt2 true 60.79 55.15 apollon059 hcai-bench/svcomp/O0/O0_string_false-unreach-call_true-termination_000.smt2 unknown 15.35 9.65 apollon020 hcai-bench/svcomp/O0/O0_vogal_true-unreach-call_000.smt2 true 183.48 176.15 apollon082 hcai-bench/svcomp/O0/O0_compact_false-unreach-call_000.smt2 TIMEOUT 1800.54 1793.40 apollon166 llreve-bench/smt2/arrays/libc__memchr_1.array_000.smt2 TIMEOUT 1800.63 1793.68 apollon031 llreve-bench/smt2/arrays/libc__stpcpy_1.array_000.smt2 TIMEOUT 1800.55 1795.23 apollon030 llreve-bench/smt2/arrays/coreutils__md5sum.array_000.smt2 true 8.24 2.21 apollon123 llreve-bench/smt2/arrays/libc__strpbrk_2.array_000.smt2 TIMEOUT 1800.59 1792.65 apollon150 llreve-bench/smt2/arrays/heap__memcpy_a.array_000.smt2 TIMEOUT 1800.53 1795.45 apollon060 llreve-bench/smt2/arrays/heap__fib.array_000.smt2 TIMEOUT 1800.59 1793.75 apollon104 llreve-bench/smt2/arrays/heap__memcpy_b.array_000.smt2 true 3.17 1.34 apollon059 llreve-bench/smt2/arrays/heap__propagate.array_000.smt2 true 3.13 1.31 apollon032 llreve-bench/smt2/arrays/heap__findmax.array_000.smt2 true 3.70 1.27 apollon123 llreve-bench/smt2/arrays/libc__memset_1.array_000.smt2 true 3.45 1.43 apollon162 llreve-bench/smt2/arrays/libc__strncmp_1.array_000.smt2 true 5.47 1.56 apollon095 llreve-bench/smt2/arrays/libc__memmove_1.array_000.smt2 true 4.81 1.40 apollon055 llreve-bench/smt2/arrays/heap__clearstr.array_000.smt2 TIMEOUT 1800.56 1794.60 apollon085 llreve-bench/smt2/arrays/libc__memccpy_1.array_000.smt2 TIMEOUT 1800.57 1794.13 apollon028 llreve-bench/smt2/arrays/libc__strcspn.array_000.smt2 true 5.12 1.66 apollon014 llreve-bench/smt2/arrays/heap__selsort.array_000.smt2 true 4.61 1.34 apollon080 llreve-bench/smt2/arrays/libc__strcmp.array_000.smt2 true 4.03 1.25 apollon059 llreve-bench/smt2/arrays/libc__strpbrk_1.array_000.smt2 true 4.56 1.46 apollon026 llreve-bench/smt2/arrays/heap__cocome2.array_000.smt2 true 13.26 4.14 apollon006 llreve-bench/smt2/arrays/libc__strchr_1.array_000.smt2 true 7.20 1.93 apollon080 llreve-bench/smt2/arrays/libc__strncmp_3.array_000.smt2 true 5.68 1.63 apollon070 llreve-bench/smt2/arrays/libc__memrchr_1.array_000.smt2 TIMEOUT 1800.63 1793.44 apollon026 llreve-bench/smt2/arrays/libc__strncmp_2.array_000.smt2 true 4.76 1.43 apollon105 llreve-bench/smt2/arrays/libc__strpbrk_3.array_000.smt2 TIMEOUT 1800.66 1791.54 apollon095 llreve-bench/muz/heap__memcpy_b_000.smt2 TIMEOUT 1800.56 1795.18 apollon003 llreve-bench/muz/heap__propagate_000.smt2 true 3.13 1.35 apollon031 llreve-bench/muz/heap__findmax_000.smt2 TIMEOUT 1800.64 1792.85 apollon068 llreve-bench/muz/libc__memccpy_1_000.smt2 TIMEOUT 1800.57 1793.91 apollon100 llreve-bench/muz/libc__stpcpy_1_000.smt2 true 3.19 1.13 apollon004 llreve-bench/muz/libc__memset_1_000.smt2 true 3.47 1.24 apollon114 llreve-bench/muz/libc__memmove_1_000.smt2 true 5.40 1.51 apollon004 llreve-bench/muz/heap__clearstr_000.smt2 TIMEOUT 1800.56 1795.52 apollon082 llreve-bench/muz/heap__memcpy_a_000.smt2 TIMEOUT 1800.55 1795.20 apollon090 llreve-bench/muz/libc__strcspn_3_000.smt2 true 5.64 1.56 apollon090 llreve-bench/muz/libc__strncmp_2_000.smt2 TIMEOUT 1800.62 1792.95 apollon101 llreve-bench/muz/heap__heap_call_000.smt2 true 3.09 1.30 apollon082 llreve-bench/muz/libc__memrchr_1_000.smt2 TIMEOUT 1800.65 1793.06 apollon131 llreve-bench/muz/libc__strcmp_000.smt2 TIMEOUT 1800.63 1792.80 apollon041 llreve-bench/muz/libc__memchr_1_000.smt2 true 4.51 1.62 apollon094 llreve-bench/muz/heap__cocome2_000.smt2 true 12.75 3.94 apollon107 llreve-bench/muz/libc__strcspn_000.smt2 true 5.53 1.61 apollon090 llreve-bench/muz/heap__swaparray_000.smt2 true 4.23 1.48 apollon030 llreve-bench/muz/libc__strpbrk_1_000.smt2 true 3.92 1.22 apollon094 llreve-bench/muz/libc__strncmp_1_000.smt2 true 5.43 1.55 apollon028 llreve-bench/muz/coreutils__remove_000.smt2 unknown 4.15 1.55 apollon107 llreve-bench/muz/libc__sbrk_1_000.smt2 true 4.70 1.57 apollon097 llreve-bench/muz/heap__fib_000.smt2 true 3.58 1.40 apollon099 llreve-bench/muz/libc__strncmp_3_000.smt2 true 5.52 1.54 apollon080 llreve-bench/muz/libc__strpbrk_3_000.smt2 true 3.97 1.22 apollon020 llreve-bench/muz/libc__strchr_1_000.smt2 true 6.95 1.89 apollon094 llreve-bench/muz/libc__memmem_1_000.smt2 unknown 5.45 1.65 apollon082 llreve-bench/muz/heap__selsort_000.smt2 true 5.24 1.51 apollon070 llreve-bench/muz/coreutils__md5sum_000.smt2 true 8.23 2.31 apollon090 llreve-bench/muz/libc__strpbrk_2_000.smt2 true 4.37 1.35 apollon004 llreve-bench/muz/libc__strcspn_2_000.smt2 unknown 5.46 1.81 apollon123 llreve-bench/unsolved/arrayOffByOne_000.smt2 TIMEOUT 1800.57 1795.00 apollon032 llreve-bench/unsolved/shiftByOne_000.smt2 TIMEOUT 1800.58 1794.82 apollon099 ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 17467.71 - Statistics: 139 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 82