BENCHMARK INFORMATION benchmark definition: ../../benchmark-defs/full-runs/pcsat.xml name: pcsat run sets: CHC-COMP2025_check-sat.LIA-Lin-Arrays date: Mon, 2025-05-05 20:06:31 CEST tool: PCSat NO_VERSION_UTIL tool executable: ./pcsat.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 TIMEOUT 1800.52 1800.50 apollon129 quic3/data/standard_palindrome_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.60 apollon056 quic3/data/standard_copy7_true-unreach-call_ground_000.smt2 TIMEOUT 1800.46 1800.55 apollon043 quic3/data/standard_init3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.48 apollon061 quic3/data/array_init_const_000.smt2 TIMEOUT 1800.51 1800.59 apollon127 quic3/data/sanfoundry_10_true-unreach-call_ground_000.smt2 TIMEOUT 1800.47 1800.54 apollon114 quic3/data/standard_partition_original_true-unreach-call_ground_000.smt2 TIMEOUT 1800.47 1800.50 apollon079 quic3/data/standard_copy5_true-unreach-call_ground_000.smt2 TIMEOUT 1800.46 1800.52 apollon158 quic3/data/standard_init5_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.56 apollon144 quic3/data/array_mul_init_true-unreach-call_1_000.smt2 TIMEOUT 1800.48 1800.48 apollon041 quic3/data/sanfoundry_27_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.61 apollon152 quic3/data/standard_copy3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.47 1800.76 apollon045 quic3/data/standard_partition_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.53 apollon155 quic3/data/standard_copy1_true-unreach-call_ground_000.smt2 TIMEOUT 1800.51 1800.58 apollon146 quic3/data/array_reverse_000.smt2 TIMEOUT 1800.50 1800.54 apollon109 quic3/data/array_nd_two_times_cell_true_000.smt2 TIMEOUT 1800.51 1800.57 apollon068 quic3/data/standard_init8_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.71 apollon051 quic3/data/standard_sort_N_nd_assert_loop_000.smt2 TIMEOUT 1800.47 1800.60 apollon016 quic3/data/standard_copy4_true-unreach-call_ground_000.smt2 TIMEOUT 1800.45 1800.63 apollon046 quic3/data/standard_copy8_true-unreach-call_ground_000.smt2 TIMEOUT 1800.46 1800.62 apollon065 quic3/data/standard_copyInitSum_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.49 apollon097 quic3/data/array_monotonic_set_000.smt2 TIMEOUT 1800.48 1800.61 apollon067 quic3/data/standard_init2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.51 apollon166 quic3/data/standard_compareModified_true-unreach-call_ground_000.smt2 TIMEOUT 1800.46 1800.60 apollon157 quic3/data/standard_maxInArray_true-unreach-call_ground_000.smt2 TIMEOUT 1800.47 1800.64 apollon101 quic3/data/standard_init6_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.54 apollon092 quic3/data/standard_vector_difference_true-unreach-call_ground_000.smt2 TIMEOUT 1800.50 1800.51 apollon126 quic3/data/standard_copy2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.47 1800.51 apollon058 quic3/data/standard_copyInitSum3_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.63 apollon038 quic3/data/standard_copy6_true-unreach-call_ground_000.smt2 TIMEOUT 1800.45 1800.56 apollon044 quic3/data/standard_find_true-unreach-call_ground_000.smt2 TIMEOUT 1800.47 1800.74 apollon104 quic3/data/standard_vararg_true-unreach-call_ground_true-termination_000.smt2 TIMEOUT 1800.51 1800.55 apollon103 quic3/data/array_init_partial_000.smt2 TIMEOUT 1800.48 1800.59 apollon039 quic3/data/standard_copyInit_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.55 apollon040 quic3/data/standard_minInArray_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.84 apollon132 quic3/data/standard_copyInitSum2_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.55 apollon003 quic3/data/standard_copy9_true-unreach-call_ground_000.smt2 TIMEOUT 1800.48 1800.52 apollon108 quic3/data/standard_init9_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.81 apollon130 quic3/data/standard_init4_true-unreach-call_ground_000.smt2 TIMEOUT 1800.50 1800.57 apollon048 quic3/data/standard_init7_true-unreach-call_ground_000.smt2 TIMEOUT 1800.49 1800.83 apollon089 quic3/data/array_swap_twice_000.smt2 TIMEOUT 1800.46 1800.64 apollon095 quic3/data/sanfoundry_02_true-unreach-call_ground_000.smt2 TIMEOUT 1800.46 1800.58 apollon060 quic3/data/array_swap_000.smt2 TIMEOUT 1800.47 1800.53 apollon082 hcai-bench/svcomp/O3/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination_000.smt2 true 0.06 0.06 apollon028 hcai-bench/svcomp/O3/eureka_01_false-unreach-call_000.smt2 TIMEOUT 1800.47 1800.72 apollon027 hcai-bench/svcomp/O3/linear_sea.ch_true-unreach-call_000.smt2 TIMEOUT 1800.49 1800.50 apollon013 hcai-bench/svcomp/O3/eureka_01_true-unreach-call_000.smt2 TIMEOUT 1800.48 1800.50 apollon074 hcai-bench/svcomp/O3/n.c40_true-unreach-call_true-termination_000.smt2 true 0.05 0.05 apollon092 hcai-bench/svcomp/O3/vogal_false-unreach-call_000.smt2 TIMEOUT 1800.47 1800.59 apollon142 hcai-bench/svcomp/O3/ludcmp_false-unreach-call_000.smt2 false 0.25 0.25 apollon145 hcai-bench/svcomp/O3/linear_search_false-unreach-call_000.smt2 false 0.23 0.23 apollon079 hcai-bench/svcomp/O3/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination_000.smt2 false 0.11 0.11 apollon142 hcai-bench/svcomp/O3/matrix_false-unreach-call_true-termination_000.smt2 false 0.34 0.34 apollon146 hcai-bench/svcomp/O3/invert_string_true-unreach-call_true-termination_000.smt2 TIMEOUT 1800.48 1800.62 apollon150 hcai-bench/svcomp/O3/while_infinite_loop_4_false-unreach-call_true-termination_000.smt2 false 0.05 0.05 apollon044 hcai-bench/svcomp/O3/insertion_sort_false-unreach-call_true-termination_000.smt2 TIMEOUT 1800.54 1800.60 apollon118 hcai-bench/svcomp/O3/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination_000.smt2 true 0.20 0.20 apollon048 hcai-bench/svcomp/O3/sum_array_false-unreach-call_000.smt2 TIMEOUT 1800.48 1800.77 apollon024 hcai-bench/svcomp/O3/invert_string_false-unreach-call_true-termination_000.smt2 TIMEOUT 1800.49 1800.56 apollon099 hcai-bench/svcomp/O3/string_true-unreach-call_true-termination_000.smt2 true 0.18 0.39 apollon043 hcai-bench/svcomp/O3/insertion_sort_true-unreach-call_true-termination_000.smt2 TIMEOUT 1800.47 1800.55 apollon002 hcai-bench/svcomp/O3/lu.cmp_true-unreach-call_000.smt2 true 0.24 0.24 apollon033 hcai-bench/svcomp/O3/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination_000.smt2 TIMEOUT 1800.57 1800.51 apollon075 hcai-bench/svcomp/O3/trex02_true-unreach-call_true-termination_000.smt2 true 0.05 0.05 apollon125 hcai-bench/svcomp/O3/string_false-unreach-call_true-termination_000.smt2 false 0.21 0.22 apollon145 hcai-bench/svcomp/O3/verisec_NetBSD-libc__loop_false-unreach-call_true-termination_000.smt2 false 0.11 0.12 apollon067 hcai-bench/svcomp/O3/nec40_true-unreach-call_true-termination_000.smt2 true 0.05 0.05 apollon079 hcai-bench/svcomp/O3/vogal_true-unreach-call_000.smt2 TIMEOUT 1800.51 1800.60 apollon113 hcai-bench/svcomp/O3/eureka_05_true-unreach-call_true-termination_000.smt2 TIMEOUT 1800.60 1800.64 apollon062 hcai-bench/svcomp/O3/sum_array_true-unreach-call_000.smt2 TIMEOUT 1800.49 1800.49 apollon021 hcai-bench/svcomp/O3/compact_false-unreach-call_000.smt2 TIMEOUT 1800.54 1800.64 apollon119 hcai-bench/svcomp/O3/trex02_false-unreach-call_true-termination_000.smt2 false 0.11 0.11 apollon079 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 true 0.22 0.22 apollon146 hcai-bench/svcomp/O0/matrix_true-unreach-call_true-termination_000.smt2 true 0.20 0.20 apollon028 hcai-bench/svcomp/O0/array_false-unreach-call_true-termination_000.smt2 false 0.13 0.13 apollon108 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 0.24 0.44 apollon052 llreve-bench/smt2/arrays/libc__stpcpy_1.array_000.smt2 true 0.20 0.20 apollon092 llreve-bench/smt2/arrays/coreutils__md5sum.array_000.smt2 true 3.59 3.59 apollon129 llreve-bench/smt2/arrays/libc__strpbrk_2.array_000.smt2 TIMEOUT 1800.49 1800.53 apollon135 llreve-bench/smt2/arrays/heap__memcpy_a.array_000.smt2 TIMEOUT 1800.47 1800.65 apollon167 llreve-bench/smt2/arrays/heap__fib.array_000.smt2 TIMEOUT 1800.48 1800.53 apollon028 llreve-bench/smt2/arrays/heap__memcpy_b.array_000.smt2 TIMEOUT 1800.49 1800.67 apollon023 llreve-bench/smt2/arrays/heap__propagate.array_000.smt2 TIMEOUT 1800.48 1800.78 apollon121 llreve-bench/smt2/arrays/heap__findmax.array_000.smt2 TIMEOUT 1800.46 1800.55 apollon052 llreve-bench/smt2/arrays/libc__memset_1.array_000.smt2 true 0.17 0.17 apollon061 llreve-bench/smt2/arrays/libc__strncmp_1.array_000.smt2 true 0.83 0.83 apollon075 llreve-bench/smt2/arrays/libc__memmove_1.array_000.smt2 true 0.53 0.53 apollon079 llreve-bench/smt2/arrays/heap__clearstr.array_000.smt2 TIMEOUT 1800.46 1800.49 apollon100 llreve-bench/smt2/arrays/libc__memccpy_1.array_000.smt2 true 0.39 0.39 apollon150 llreve-bench/smt2/arrays/libc__strcspn.array_000.smt2 TIMEOUT 1800.51 1800.50 apollon156 llreve-bench/smt2/arrays/heap__selsort.array_000.smt2 TIMEOUT 1800.47 1800.55 apollon141 llreve-bench/smt2/arrays/libc__strcmp.array_000.smt2 true 0.53 0.53 apollon016 llreve-bench/smt2/arrays/libc__strpbrk_1.array_000.smt2 true 30.52 30.52 apollon068 llreve-bench/smt2/arrays/heap__cocome2.array_000.smt2 true 213.55 213.56 apollon128 llreve-bench/smt2/arrays/libc__strchr_1.array_000.smt2 true 13.71 13.71 apollon062 llreve-bench/smt2/arrays/libc__strncmp_3.array_000.smt2 true 0.45 0.46 apollon166 llreve-bench/smt2/arrays/libc__memrchr_1.array_000.smt2 true 0.25 0.46 apollon167 llreve-bench/smt2/arrays/libc__strncmp_2.array_000.smt2 true 0.43 0.43 apollon039 llreve-bench/smt2/arrays/libc__strpbrk_3.array_000.smt2 true 0.57 0.58 apollon044 llreve-bench/muz/heap__memcpy_b_000.smt2 TIMEOUT 1800.47 1800.58 apollon019 llreve-bench/muz/heap__propagate_000.smt2 TIMEOUT 1800.49 1800.54 apollon168 llreve-bench/muz/heap__findmax_000.smt2 TIMEOUT 1800.46 1800.55 apollon057 llreve-bench/muz/libc__memccpy_1_000.smt2 true 0.65 0.65 apollon062 llreve-bench/muz/libc__stpcpy_1_000.smt2 true 0.20 0.20 apollon003 llreve-bench/muz/libc__memset_1_000.smt2 true 0.17 0.17 apollon048 llreve-bench/muz/libc__memmove_1_000.smt2 true 0.41 0.42 apollon167 llreve-bench/muz/heap__clearstr_000.smt2 TIMEOUT 1800.46 1800.57 apollon098 llreve-bench/muz/heap__memcpy_a_000.smt2 TIMEOUT 1800.47 1800.59 apollon147 llreve-bench/muz/libc__strcspn_3_000.smt2 TIMEOUT 1800.50 1800.50 apollon063 llreve-bench/muz/libc__strncmp_2_000.smt2 true 0.53 0.53 apollon146 llreve-bench/muz/heap__heap_call_000.smt2 true 0.05 0.05 apollon048 llreve-bench/muz/libc__memrchr_1_000.smt2 true 0.27 0.50 apollon097 llreve-bench/muz/libc__strcmp_000.smt2 true 0.62 0.62 apollon048 llreve-bench/muz/libc__memchr_1_000.smt2 true 0.19 0.20 apollon098 llreve-bench/muz/heap__cocome2_000.smt2 true 842.30 842.37 apollon036 llreve-bench/muz/libc__strcspn_000.smt2 TIMEOUT 1800.51 1800.46 apollon145 llreve-bench/muz/heap__swaparray_000.smt2 TIMEOUT 1800.46 1800.56 apollon035 llreve-bench/muz/libc__strpbrk_1_000.smt2 true 6.21 6.21 apollon139 llreve-bench/muz/libc__strncmp_1_000.smt2 true 0.72 0.75 apollon095 llreve-bench/muz/coreutils__remove_000.smt2 false 0.07 0.07 apollon007 llreve-bench/muz/libc__sbrk_1_000.smt2 true 0.20 0.20 apollon046 llreve-bench/muz/heap__fib_000.smt2 TIMEOUT 1800.48 1800.58 apollon015 llreve-bench/muz/libc__strncmp_3_000.smt2 true 0.41 0.42 apollon013 llreve-bench/muz/libc__strpbrk_3_000.smt2 true 0.58 0.58 apollon146 llreve-bench/muz/libc__strchr_1_000.smt2 true 10.16 10.16 apollon167 llreve-bench/muz/libc__memmem_1_000.smt2 false 0.15 0.16 apollon155 llreve-bench/muz/heap__selsort_000.smt2 TIMEOUT 1800.49 1800.63 apollon133 llreve-bench/muz/coreutils__md5sum_000.smt2 true 3.33 3.34 apollon058 llreve-bench/muz/libc__strpbrk_2_000.smt2 TIMEOUT 1800.48 1800.57 apollon112 llreve-bench/muz/libc__strcspn_2_000.smt2 TIMEOUT 1800.46 1800.62 apollon139 llreve-bench/unsolved/arrayOffByOne_000.smt2 TIMEOUT 1800.47 1800.63 apollon004 llreve-bench/unsolved/shiftByOne_000.smt2 TIMEOUT 1800.47 1800.58 apollon080 ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 2402.58 - Statistics: 132 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 80