ukojak.2017-01-14_0629.results.sv-comp17.MemSafety-LinkedLists.xml.bz2.merged.xml.bz2

Tool	ULTIMATE Kojak f7c3ed31
Limits	timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host	apollon*
OS	Linux 4.4.0-59-generic
System	CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution	2017-01-14 06:29:29 CET [[ 2017-01-15 05:44:30 CET ]] [[ 2017-01-15 05:59:35 CET ]] [[ 2017-01-15 05:44:48 CET ]] [[ 2017-01-15 06:00:32 CET ]]
Run set	sv-comp17.MemSafety-LinkedLists
Options	[[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/	verifier status	score	witness	inspect witness	cpu (s)	wall (s)	energy (J)	mem (MB)	blkio-w (MB)	blkio-r (MB)	validator cpachecker violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator cpachecker correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	13000	1300	2.3	0	-					-					error (invalid witness file)	.51	.34	12	40	error (invalid witness file)	5.9	3.2	120	290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	830	9900	2100	2.3	0	-					-					error (invalid witness file)	.50	.33	12	40	error (invalid witness file)	5.9	3.1	120	300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	13000	1200	2.3	0	-					-					error (invalid witness file)	.52	.35	12	40	error (invalid witness file)	6.3	3.3	140	310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	830	12000	1900	2.3	0	-					-					error (invalid witness file)	.57	.37	10	40	error (invalid witness file)	6.3	3.4	130	310
heap-manipulation/tree_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	570	510	8000	1800	2.5	0	exception	3.2	1.7	32	180	false(valid-deref)	13	6.7	190	370	-					-
heap-manipulation/tree_false-valid-deref.i	false(valid-deref)	1	wit	inspect	7.7	2.3	56	340	2.5	0	false(valid-deref)	5.1	2.7	59	270	true	9.4	5.0	160	350	-					-
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	820	12000	1300	2.3	0	error (invalid witness file)	.54	.34	12	40	error (invalid witness file)	6.8	3.6	86	290	-					-
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i	error	0	wit	inspect	8.5	2.8	66	310	2.6	0	error (invalid witness file)	.51	.33	10	41	error (invalid witness file)	5.8	3.1	120	310	-					-
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	820	11000	1700	2.3	0	error (invalid witness file)	.53	.35	7.5	43	error (invalid witness file)	6.2	3.3	130	300	-					-
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	810	11000	1700	2.3	0	error (invalid witness file)	.53	.35	13	39	error (invalid witness file)	6.2	3.3	130	310	-					-
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	14000	2100	2.3	0	-					-					error (invalid witness file)	.61	.39	8.6	39	error (invalid witness file)	5.7	3.0	110	290
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i	unknown	0	wit	inspect	30	14	290	640	2.6	0	error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	6.3	3.3	130	300	-					-
list-properties/list_search_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	830	11000	1000	2.3	0	error (invalid witness file)	.53	.35	12	41	error (invalid witness file)	6.2	3.3	120	300	-					-
list-properties/list_true-unreach-call_false-valid-memtrack.i	unknown	0	wit	inspect	46	24	470	710	2.6	0	error (invalid witness file)	.57	.37	11	42	error (invalid witness file)	6.2	3.3	120	310	-					-
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i	unknown	0	wit	inspect	24	11	250	500	2.6	0	error (invalid witness file)	.58	.36	13	41	error (invalid witness file)	6.0	3.2	120	300	-					-
list-properties/simple_true-unreach-call_false-valid-memtrack.i	unknown	0	wit	inspect	42	24	530	710	2.6	0	error (invalid witness file)	.54	.34	12	40	error (invalid witness file)	6.1	3.3	130	300	-					-
list-properties/splice_true-unreach-call_false-valid-memtrack.i	unknown	0	wit	inspect	20	6.5	170	500	2.6	0	error (invalid witness file)	.65	.40	6.7	40	error (invalid witness file)	5.9	3.1	120	300	-					-
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i	true	2	wit	inspect	410	340	5400	5000	3.2	0	-					-					true	8.8	4.6	110	320	true	210	170	1400	1900
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i	true	2	wit	inspect	410	340	5300	5400	3.0	0	-					-					true	9.8	5.0	160	320	true	210	160	3900	1700
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i	true	2	wit	inspect	410	350	6200	5300	3.1	0	-					-					true	9.0	4.7	120	320	true	200	160	2000	1800
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	810	11000	7000	2.3	0	error (invalid witness file)	.55	.35	11	40	error (invalid witness file)	6.2	3.3	130	300	-					-
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	830	12000	5800	2.3	0	error (invalid witness file)	.52	.35	12	39	error (invalid witness file)	7.9	4.1	100	300	-					-
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	820	9600	6400	2.5	0	error (invalid witness file)	.50	.32	7.8	39	error (invalid witness file)	6.8	3.6	120	310	-					-
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i	error	0	wit	inspect	530	460	6800	6900	2.5	0	error (invalid witness file)	.54	.36	13	40	error (invalid witness file)	6.1	3.3	120	290	-					-
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i	error	0	wit	inspect	480	410	6400	6700	2.5	0	error (invalid witness file)	.50	.31	10	40	error (invalid witness file)	6.4	3.4	130	300	-					-
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	830	11000	6000	2.3	0	error (invalid witness file)	.55	.34	12	39	error (invalid witness file)	6.3	3.3	120	300	-					-
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i	error	0	wit	inspect	560	490	7500	7100	2.5	0	error (invalid witness file)	.54	.35	12	40	error (invalid witness file)	7.0	3.6	150	320	-					-
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	830	10000	6100	2.3	0	error (invalid witness file)	.51	.33	11	41	error (invalid witness file)	6.0	3.2	120	310	-					-
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i	error	0	wit	inspect	550	480	7000	6800	2.5	.016	error (invalid witness file)	.54	.36	12	39	error (invalid witness file)	6.4	3.4	130	300	-					-
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	830	11000	6100	2.5	.090	error (invalid witness file)	.62	.39	8.2	40	error (invalid witness file)	6.2	3.3	120	300	-					-
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	11000	1300	2.3	0	-					-					error (invalid witness file)	.54	.34	12	42	error (invalid witness file)	6.4	3.4	140	310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	12000	1700	2.3	0	-					-					error (invalid witness file)	.53	.35	11	40	error (invalid witness file)	6.1	3.2	120	290
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	800	12000	1400	2.3	0	-					-					error (invalid witness file)	.53	.34	13	40	error (invalid witness file)	5.8	3.1	99	290
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	830	12000	1600	2.3	0	-					-					error (invalid witness file)	.54	.34	12	40	error (invalid witness file)	5.9	3.1	120	290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	14000	1500	2.3	0	-					-					error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	6.4	3.3	140	300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i	error	0	wit	inspect	8.3	2.7	85	300	2.6	0	-					-					error (invalid witness file)	.52	.33	10	40	error (invalid witness file)	6.0	3.1	120	300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	12000	1700	2.3	0	-					-					error (invalid witness file)	.53	.35	12	39	error (invalid witness file)	5.8	3.1	130	300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	12000	1600	2.3	0	-					-					error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	6.2	3.2	140	300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	11000	1600	2.3	0	-					-					error (invalid witness file)	.50	.32	9.1	39	error (invalid witness file)	6.7	3.5	130	310
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	12000	1700	2.3	0	-					-					error (invalid witness file)	.51	.33	11	42	error (invalid witness file)	5.7	3.1	120	300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	12000	2400	2.3	0	-					-					error (invalid witness file)	.54	.36	11	40	error (invalid witness file)	6.6	3.4	120	320
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	11000	1900	2.3	0	-					-					error (invalid witness file)	.57	.37	9.3	40	error (invalid witness file)	5.9	3.2	120	300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	14000	1700	2.3	0	-					-					error (invalid witness file)	.48	.32	11	40	error (invalid witness file)	6.2	3.2	120	300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	14000	1700	2.3	0	-					-					error (invalid witness file)	.51	.33	11	40	error (invalid witness file)	6.3	3.4	120	300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	15000	1300	2.3	0	-					-					error (invalid witness file)	.51	.33	11	41	error (invalid witness file)	6.6	3.4	130	310
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i	error	0	wit	inspect	9.1	2.7	72	340	2.6	0	-					-					error (invalid witness file)	.52	.35	12	39	error (invalid witness file)	5.7	3.1	120	290
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	13000	1700	2.7	0	-					-					error (invalid witness file)	.61	.39	8.8	40	error (invalid witness file)	6.3	3.3	130	300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	810	11000	1400	2.3	0	-					-					error (invalid witness file)	.57	.36	9.4	41	error (invalid witness file)	6.8	3.6	130	320
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	820	14000	1200	2.3	0	-					-					error (invalid witness file)	.53	.34	11	40	error (invalid witness file)	6.3	3.3	130	310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i	timeout	0	wit	inspect	900	820	13000	3400	2.3	0	error (invalid witness file)	.51	.33	9.1	40	error (invalid witness file)	6.5	3.4	130	300	-					-
forester-heap/sll-01_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	260	220	3500	1500	2.5	0	true	5.2	2.8	82	270	true	18	9.7	260	500	-					-
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	260	220	4200	1400	2.5	0	true	4.9	2.7	58	260	false(valid-deref)	11	5.7	190	370	-					-
../../sv-benchmarks/c/	verifier status	score	witness	inspect witness	cpu (s)	wall (s)	energy (J)	mem (MB)	blkio-w (MB)	blkio-r (MB)	validator cpachecker violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator cpachecker correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)
total	52	10			34000	31000	460000	130000	130	.11	52	30	17	460	1800	52	180	98	3400	7900	52	40	23	640	1900	52	770	580	10000	13000
correct results	7	10			2300	2000	33000	21000	19	0	3	18	10	230	980	4	51	27	810	1600	3	28	14	380	970	3	620	500	7300	5300
correct true	3	6			1200	1000	17000	16000	9.3	0	2	0	0	0	0	2	0	0	0	0	3	28	14	380	970	3	620	500	7300	5300
correct false	4	4			1100	960	16000	5100	10	0	1	18	10	230	980	2	51	27	810	1600	0	0	0	0	0	0	0	0	0	0
correct-unconfimed results	0
correct-unconfirmed true	0
correct-unconfirmed false	0
incorrect results	0
incorrect true	0
incorrect false	0
score (52 tasks, max score: 79)	10
Run set	sv-comp17.MemSafety-LinkedLists