BENCHMARK INFORMATION benchmark definition: ../../benchmark-defs/pre-runs/theta.xml name: theta run sets: CHC-COMP2025_check-sat.LIA-Lin-Arrays date: Mon, 2025-05-05 21:25:53 CEST tool: ThetaCHC 6.13.2 tool executable: ./chc options: resource limits: - memory: 7000.0 MB - time: 60 s - cpu cores: 2 hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz - cpu cores: 2 - memory: 7000.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 60.39 55.86 apollon023 quic3/data/standard_palindrome_true-unreach-call_ground_000.smt2 TIMEOUT 60.35 56.41 apollon136 quic3/data/standard_copy7_true-unreach-call_ground_000.smt2 TIMEOUT 60.60 53.18 apollon046 quic3/data/standard_init3_true-unreach-call_ground_000.smt2 TIMEOUT 60.52 55.97 apollon015 quic3/data/array_init_const_000.smt2 TIMEOUT 60.34 56.49 apollon055 quic3/data/sanfoundry_10_true-unreach-call_ground_000.smt2 TIMEOUT 60.46 54.81 apollon136 quic3/data/standard_partition_original_true-unreach-call_ground_000.smt2 TIMEOUT 60.40 55.43 apollon123 quic3/data/standard_copy5_true-unreach-call_ground_000.smt2 TIMEOUT 60.49 54.43 apollon133 quic3/data/standard_init5_true-unreach-call_ground_000.smt2 TIMEOUT 60.41 55.66 apollon076 quic3/data/array_mul_init_true-unreach-call_1_000.smt2 TIMEOUT 60.42 55.36 apollon055 quic3/data/sanfoundry_27_true-unreach-call_ground_000.smt2 TIMEOUT 60.38 56.13 apollon017 quic3/data/standard_copy3_true-unreach-call_ground_000.smt2 TIMEOUT 60.43 55.39 apollon055 quic3/data/standard_partition_true-unreach-call_ground_000.smt2 TIMEOUT 60.44 55.17 apollon072 quic3/data/standard_copy1_true-unreach-call_ground_000.smt2 TIMEOUT 60.35 56.36 apollon112 quic3/data/array_reverse_000.smt2 TIMEOUT 60.40 55.74 apollon015 quic3/data/array_nd_two_times_cell_true_000.smt2 TIMEOUT 60.33 56.47 apollon133 quic3/data/standard_init8_true-unreach-call_ground_000.smt2 TIMEOUT 60.50 54.53 apollon127 quic3/data/standard_sort_N_nd_assert_loop_000.smt2 TIMEOUT 60.33 56.69 apollon136 quic3/data/standard_copy4_true-unreach-call_ground_000.smt2 TIMEOUT 60.44 55.07 apollon072 quic3/data/standard_copy8_true-unreach-call_ground_000.smt2 TIMEOUT 60.63 52.85 apollon015 quic3/data/standard_copyInitSum_true-unreach-call_ground_000.smt2 TIMEOUT 60.42 55.36 apollon127 quic3/data/array_monotonic_set_000.smt2 TIMEOUT 60.37 56.31 apollon127 quic3/data/standard_init2_true-unreach-call_ground_000.smt2 TIMEOUT 60.40 56.29 apollon072 quic3/data/standard_compareModified_true-unreach-call_ground_000.smt2 TIMEOUT 60.40 55.60 apollon017 quic3/data/standard_maxInArray_true-unreach-call_ground_000.smt2 TIMEOUT 60.37 56.25 apollon133 quic3/data/standard_init6_true-unreach-call_ground_000.smt2 TIMEOUT 60.45 55.12 apollon015 quic3/data/standard_vector_difference_true-unreach-call_ground_000.smt2 TIMEOUT 60.40 56.06 apollon112 quic3/data/standard_copy2_true-unreach-call_ground_000.smt2 TIMEOUT 60.43 55.20 apollon020 quic3/data/standard_copyInitSum3_true-unreach-call_ground_000.smt2 TIMEOUT 60.41 55.65 apollon123 quic3/data/standard_copy6_true-unreach-call_ground_000.smt2 TIMEOUT 60.55 53.48 apollon127 quic3/data/standard_find_true-unreach-call_ground_000.smt2 TIMEOUT 60.36 56.18 apollon112 quic3/data/standard_vararg_true-unreach-call_ground_true-termination_000.smt2 TIMEOUT 60.34 56.43 apollon020 quic3/data/array_init_partial_000.smt2 TIMEOUT 60.46 54.57 apollon015 quic3/data/standard_copyInit_true-unreach-call_ground_000.smt2 TIMEOUT 60.40 55.58 apollon046 quic3/data/standard_minInArray_true-unreach-call_ground_000.smt2 TIMEOUT 60.38 55.91 apollon127 quic3/data/standard_copyInitSum2_true-unreach-call_ground_000.smt2 TIMEOUT 60.37 56.18 apollon072 quic3/data/standard_copy9_true-unreach-call_ground_000.smt2 TIMEOUT 60.62 52.56 apollon015 quic3/data/standard_init9_true-unreach-call_ground_000.smt2 TIMEOUT 60.46 54.99 apollon020 quic3/data/standard_init4_true-unreach-call_ground_000.smt2 TIMEOUT 60.43 55.51 apollon046 quic3/data/standard_init7_true-unreach-call_ground_000.smt2 TIMEOUT 60.53 53.91 apollon112 quic3/data/array_swap_twice_000.smt2 TIMEOUT 60.43 55.15 apollon051 quic3/data/sanfoundry_02_true-unreach-call_ground_000.smt2 TIMEOUT 60.43 55.30 apollon046 quic3/data/array_swap_000.smt2 TIMEOUT 60.43 55.18 apollon020 hcai-bench/svcomp/O3/O3_veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 true 7.51 4.32 apollon076 hcai-bench/svcomp/O3/O3_eureka_01_false-unreach-call_000.smt2 unknown 30.93 22.99 apollon136 hcai-bench/svcomp/O3/O3_linear_sea.ch_true-unreach-call_000.smt2 unknown 4.60 2.45 apollon072 hcai-bench/svcomp/O3/O3_eureka_01_true-unreach-call_000.smt2 TIMEOUT 60.55 53.35 apollon123 hcai-bench/svcomp/O3/O3_n.c40_true-unreach-call_true-termination_000.smt2 true 3.56 2.14 apollon020 hcai-bench/svcomp/O3/O3_vogal_false-unreach-call_000.smt2 unknown 15.54 10.06 apollon023 hcai-bench/svcomp/O3/O3_ludcmp_false-unreach-call_000.smt2 true 6.47 3.45 apollon136 hcai-bench/svcomp/O3/O3_linear_search_false-unreach-call_000.smt2 unknown 4.84 2.76 apollon133 hcai-bench/svcomp/O3/O3_veris.c_NetBSD-libc__loop_true-unreach-call_true-termination_000.smt2 true 4.63 2.46 apollon055 hcai-bench/svcomp/O3/O3_matrix_false-unreach-call_true-termination_000.smt2 false 8.35 4.33 apollon051 hcai-bench/svcomp/O3/O3_invert_string_true-unreach-call_true-termination_000.smt2 true 6.24 3.50 apollon133 hcai-bench/svcomp/O3/O3_while_infinite_loop_4_false-unreach-call_true-termination_000.smt2 unknown 3.82 2.29 apollon046 hcai-bench/svcomp/O3/O3_insertion_sort_false-unreach-call_true-termination_000.smt2 true 7.99 4.17 apollon017 hcai-bench/svcomp/O3/O3_veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination_000.smt2 TIMEOUT 60.50 54.20 apollon023 hcai-bench/svcomp/O3/O3_sum_array_false-unreach-call_000.smt2 false 11.11 5.98 apollon136 hcai-bench/svcomp/O3/O3_invert_string_false-unreach-call_true-termination_000.smt2 false 11.25 6.47 apollon123 hcai-bench/svcomp/O3/O3_string_true-unreach-call_true-termination_000.smt2 true 29.22 24.67 apollon072 hcai-bench/svcomp/O3/O3_insertion_sort_true-unreach-call_true-termination_000.smt2 true 8.70 4.50 apollon046 hcai-bench/svcomp/O3/O3_lu.cmp_true-unreach-call_000.smt2 true 7.34 3.81 apollon055 hcai-bench/svcomp/O3/O3_verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination_000.smt2 unknown 16.41 9.15 apollon103 hcai-bench/svcomp/O3/O3_trex02_true-unreach-call_true-termination_000.smt2 TIMEOUT 60.40 55.66 apollon103 hcai-bench/svcomp/O3/O3_string_false-unreach-call_true-termination_000.smt2 unknown 10.13 5.88 apollon017 hcai-bench/svcomp/O3/O3_verisec_NetBSD-libc__loop_false-unreach-call_true-termination_000.smt2 false 4.44 2.38 apollon020 hcai-bench/svcomp/O3/O3_nec40_true-unreach-call_true-termination_000.smt2 true 3.64 2.16 apollon072 hcai-bench/svcomp/O3/O3_vogal_true-unreach-call_000.smt2 true 16.38 11.18 apollon136 hcai-bench/svcomp/O3/O3_eureka_05_true-unreach-call_true-termination_000.smt2 true 8.21 4.73 apollon127 hcai-bench/svcomp/O3/O3_sum_array_true-unreach-call_000.smt2 TIMEOUT 60.58 52.98 apollon046 hcai-bench/svcomp/O3/O3_compact_false-unreach-call_000.smt2 TIMEOUT 60.39 55.79 apollon123 hcai-bench/svcomp/O3/O3_trex02_false-unreach-call_true-termination_000.smt2 unknown 4.56 2.44 apollon112 hcai-bench/svcomp/O0/O0_veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 true 9.76 6.05 apollon076 hcai-bench/svcomp/O0/O0_n.c40_true-unreach-call_true-termination_000.smt2 TIMEOUT 60.49 54.55 apollon017 hcai-bench/svcomp/O0/O0_vogal_false-unreach-call_000.smt2 TIMEOUT 60.43 55.06 apollon076 hcai-bench/svcomp/O0/O0_array_true-unreach-call_true-termination_000.smt2 true 4.04 2.15 apollon076 hcai-bench/svcomp/O0/O0_matrix_true-unreach-call_true-termination_000.smt2 true 5.03 2.82 apollon112 hcai-bench/svcomp/O0/O0_array_false-unreach-call_true-termination_000.smt2 unknown 5.85 3.25 apollon015 hcai-bench/svcomp/O0/O0_string_true-unreach-call_true-termination_000.smt2 TIMEOUT 60.52 53.81 apollon046 hcai-bench/svcomp/O0/O0_string_false-unreach-call_true-termination_000.smt2 unknown 19.63 13.40 apollon051 hcai-bench/svcomp/O0/O0_vogal_true-unreach-call_000.smt2 TIMEOUT 60.58 53.52 apollon051 hcai-bench/svcomp/O0/O0_compact_false-unreach-call_000.smt2 TIMEOUT 60.32 56.59 apollon103 llreve-bench/smt2/arrays/libc__memchr_1.array_000.smt2 TIMEOUT 60.45 55.46 apollon127 llreve-bench/smt2/arrays/libc__stpcpy_1.array_000.smt2 TIMEOUT 60.35 56.33 apollon123 llreve-bench/smt2/arrays/coreutils__md5sum.array_000.smt2 true 9.59 4.94 apollon127 llreve-bench/smt2/arrays/libc__strpbrk_2.array_000.smt2 TIMEOUT 60.44 55.97 apollon017 llreve-bench/smt2/arrays/heap__memcpy_a.array_000.smt2 TIMEOUT 60.39 56.44 apollon015 llreve-bench/smt2/arrays/heap__fib.array_000.smt2 TIMEOUT 60.37 56.44 apollon133 llreve-bench/smt2/arrays/heap__memcpy_b.array_000.smt2 true 4.02 2.31 apollon136 llreve-bench/smt2/arrays/heap__propagate.array_000.smt2 true 3.85 2.05 apollon072 llreve-bench/smt2/arrays/heap__findmax.array_000.smt2 true 4.87 2.57 apollon127 llreve-bench/smt2/arrays/libc__memset_1.array_000.smt2 true 4.44 2.36 apollon055 llreve-bench/smt2/arrays/libc__strncmp_1.array_000.smt2 true 6.71 3.53 apollon123 llreve-bench/smt2/arrays/libc__memmove_1.array_000.smt2 true 5.60 2.93 apollon015 llreve-bench/smt2/arrays/heap__clearstr.array_000.smt2 TIMEOUT 60.35 56.25 apollon055 llreve-bench/smt2/arrays/libc__memccpy_1.array_000.smt2 TIMEOUT 60.42 56.12 apollon123 llreve-bench/smt2/arrays/libc__strcspn.array_000.smt2 true 5.83 3.08 apollon023 llreve-bench/smt2/arrays/heap__selsort.array_000.smt2 true 5.43 2.86 apollon055 llreve-bench/smt2/arrays/libc__strcmp.array_000.smt2 true 5.55 3.00 apollon015 llreve-bench/smt2/arrays/libc__strpbrk_1.array_000.smt2 true 5.04 2.71 apollon015 llreve-bench/smt2/arrays/heap__cocome2.array_000.smt2 true 16.51 8.43 apollon133 llreve-bench/smt2/arrays/libc__strchr_1.array_000.smt2 true 7.91 4.09 apollon112 llreve-bench/smt2/arrays/libc__strncmp_3.array_000.smt2 true 5.51 2.93 apollon020 llreve-bench/smt2/arrays/libc__memrchr_1.array_000.smt2 TIMEOUT 60.47 55.31 apollon133 llreve-bench/smt2/arrays/libc__strncmp_2.array_000.smt2 true 5.87 3.08 apollon136 llreve-bench/smt2/arrays/libc__strpbrk_3.array_000.smt2 TIMEOUT 60.57 54.34 apollon103 llreve-bench/muz/heap__memcpy_b_000.smt2 TIMEOUT 60.34 57.26 apollon020 llreve-bench/muz/heap__propagate_000.smt2 true 4.03 2.14 apollon020 llreve-bench/muz/heap__findmax_000.smt2 TIMEOUT 60.40 56.09 apollon072 llreve-bench/muz/libc__memccpy_1_000.smt2 TIMEOUT 60.39 56.44 apollon103 llreve-bench/muz/libc__stpcpy_1_000.smt2 true 4.30 2.28 apollon055 llreve-bench/muz/libc__memset_1_000.smt2 true 4.12 2.32 apollon023 llreve-bench/muz/libc__memmove_1_000.smt2 true 5.15 2.71 apollon076 llreve-bench/muz/heap__clearstr_000.smt2 TIMEOUT 60.42 55.35 apollon015 llreve-bench/muz/heap__memcpy_a_000.smt2 TIMEOUT 60.34 56.72 apollon051 llreve-bench/muz/libc__strcspn_3_000.smt2 true 6.59 3.58 apollon046 llreve-bench/muz/libc__strncmp_2_000.smt2 TIMEOUT 60.42 55.53 apollon136 llreve-bench/muz/heap__heap_call_000.smt2 true 3.89 2.27 apollon051 llreve-bench/muz/libc__memrchr_1_000.smt2 TIMEOUT 60.44 55.81 apollon051 llreve-bench/muz/libc__strcmp_000.smt2 TIMEOUT 60.55 55.03 apollon076 llreve-bench/muz/libc__memchr_1_000.smt2 true 4.59 2.42 apollon023 llreve-bench/muz/heap__cocome2_000.smt2 true 16.00 8.36 apollon103 llreve-bench/muz/libc__strcspn_000.smt2 true 5.95 3.13 apollon055 llreve-bench/muz/heap__swaparray_000.smt2 true 4.52 2.39 apollon020 llreve-bench/muz/libc__strpbrk_1_000.smt2 true 5.34 2.82 apollon046 llreve-bench/muz/libc__strncmp_1_000.smt2 true 6.06 3.16 apollon055 llreve-bench/muz/coreutils__remove_000.smt2 unknown 4.67 2.51 apollon055 llreve-bench/muz/libc__sbrk_1_000.smt2 true 5.00 2.63 apollon020 llreve-bench/muz/heap__fib_000.smt2 true 4.25 2.44 apollon055 llreve-bench/muz/libc__strncmp_3_000.smt2 true 5.39 2.88 apollon133 llreve-bench/muz/libc__strpbrk_3_000.smt2 true 4.98 2.65 apollon051 llreve-bench/muz/libc__strchr_1_000.smt2 true 8.13 4.31 apollon127 llreve-bench/muz/libc__memmem_1_000.smt2 unknown 5.47 3.09 apollon020 llreve-bench/muz/heap__selsort_000.smt2 true 5.11 2.68 apollon055 llreve-bench/muz/coreutils__md5sum_000.smt2 true 9.13 4.99 apollon020 llreve-bench/muz/libc__strpbrk_2_000.smt2 true 4.82 2.55 apollon112 llreve-bench/muz/libc__strcspn_2_000.smt2 unknown 6.31 3.45 apollon046 llreve-bench/unsolved/arrayOffByOne_000.smt2 TIMEOUT 60.31 56.90 apollon020 llreve-bench/unsolved/shiftByOne_000.smt2 TIMEOUT 60.32 56.67 apollon112 ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 334.84 - Statistics: 139 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 85