esbmc-falsi.2017-01-13_0520.results.sv-comp17.MemSafety-LinkedLists.xml.bz2.merged.xml.bz2

Tool	ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-13 05:20:12 CET [[ 2017-01-15 00:51:08 CET ]] [[ 2017-01-15 01:00:54 CET ]] [[ 2017-01-15 00:55:05 CET ]] [[ 2017-01-15 01:06:26 CET ]]
Run set	sv-comp17.MemSafety-LinkedLists
Options	-s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.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	900	10000	1900	.99	0	-					-					error (invalid witness file)	.50	.32	12	41	error (invalid witness file)	6.1	3.2	110	290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	11000	830	.84	0	-					-					error (invalid witness file)	.58	.37	7.7	43	error (invalid witness file)	7.7	4.0	110	340
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	12000	1100	.95	0	-					-					error (invalid witness file)	.52	.34	5.3	40	error (invalid witness file)	5.9	3.1	96	310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	12000	430	.99	0	-					-					error (invalid witness file)	.50	.32	6.0	39	error (invalid witness file)	6.2	3.3	95	310
heap-manipulation/tree_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	.31	.31	3.4	25	.84	0	error (invalid witness file)	.51	.33	12	39	error (invalid witness file)	5.3	2.9	84	290	-					-
heap-manipulation/tree_false-valid-deref.i	false(valid-deref)	1	wit	inspect	.15	.15	1.1	25	.99	0	error (invalid witness file)	.54	.36	12	39	error (invalid witness file)	6.1	3.2	89	290	-					-
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.18	.18	1.8	25	.99	0	error (invalid witness file)	.50	.33	12	39	error (invalid witness file)	5.9	3.1	110	300	-					-
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	1.8	1.8	4.0	32	.99	0	error (invalid witness file)	.51	.33	8.9	40	error (invalid witness file)	5.7	3.0	79	300	-					-
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.32	.32	3.2	30	.84	0	error (invalid witness file)	.51	.33	8.7	41	error (invalid witness file)	5.2	2.8	79	290	-					-
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.25	.25	2.9	26	.84	0	error (invalid witness file)	.55	.36	12	40	error (invalid witness file)	5.6	3.0	73	290	-					-
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9700	1400	.99	0	-					-					error (invalid witness file)	.51	.35	9.6	39	error (invalid witness file)	6.2	3.3	110	300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.16	.15	1.3	24	.85	0	error (invalid witness file)	.50	.31	11	39	error (invalid witness file)	5.6	3.0	86	300	-					-
list-properties/list_search_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.28	.28	3.3	25	.99	0	error (invalid witness file)	.53	.34	11	40	error (invalid witness file)	6.1	3.2	97	310	-					-
list-properties/list_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.13	.13	1.4	24	.84	0	error (invalid witness file)	.50	.31	8.2	40	error (invalid witness file)	6.6	3.5	110	320	-					-
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.16	.16	1.3	24	.99	0	error (invalid witness file)	.55	.35	11	39	error (invalid witness file)	5.9	3.1	99	310	-					-
list-properties/simple_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.13	.13	1.5	24	.99	0	error (invalid witness file)	.50	.33	11	40	error (invalid witness file)	5.9	3.2	120	290	-					-
list-properties/splice_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	.12	.12	1.4	25	.95	0	error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	5.7	3.0	84	300	-					-
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i	false(valid-memtrack)	-16	wit	inspect	230	230	2200	840	.99	0	-					-					error (invalid witness file)	.57	.37	7.9	39	error (invalid witness file)	6.3	3.3	94	300
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i	false(valid-memtrack)	-16	wit	inspect	590	590	6900	850	.99	0	-					-					error (invalid witness file)	.50	.32	4.8	40	error (invalid witness file)	6.0	3.2	70	290
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i	false(valid-memtrack)	-16	wit	inspect	300	300	3400	630	.84	0	-					-					error (invalid witness file)	.49	.32	11	39	error (invalid witness file)	5.7	3.1	96	290
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	800	800	8500	1100	.84	0	error (invalid witness file)	.50	.33	11	39	error (invalid witness file)	6.7	3.5	140	300	-					-
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	1900	460	.99	0	error (invalid witness file)	.52	.34	10	44	error (invalid witness file)	6.4	3.4	100	300	-					-
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	13000	920	.99	0	error (invalid witness file)	.53	.34	12	40	error (invalid witness file)	6.1	3.3	100	300	-					-
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	9600	800	.99	0	error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	6.5	3.4	110	300	-					-
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	13000	760	.84	0	error (invalid witness file)	.53	.34	12	40	error (invalid witness file)	6.2	3.3	100	300	-					-
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i	false(valid-memtrack)	1	wit	inspect	660	660	8900	820	.99	0	error (invalid witness file)	.52	.33	12	40	error (invalid witness file)	6.5	3.4	87	300	-					-
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	11000	1000	.99	0	error (invalid witness file)	.49	.32	8.3	40	error (invalid witness file)	6.2	3.3	110	310	-					-
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	9900	870	.84	0	error (invalid witness file)	.54	.36	12	41	error (invalid witness file)	6.4	3.4	80	310	-					-
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	12000	760	.99	0	error (invalid witness file)	.48	.31	9.0	39	error (invalid witness file)	7.9	4.1	120	330	-					-
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i	timeout	0	wit	inspect	900	900	10000	1100	.84	0	error (invalid witness file)	.52	.33	12	40	error (invalid witness file)	6.2	3.3	100	290	-					-
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	10000	600	.99	0	-					-					error (invalid witness file)	.50	.34	9.4	40	error (invalid witness file)	6.2	3.3	91	300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	11000	11000	.84	0	-					-					error (invalid witness file)	.50	.34	6.8	39	error (invalid witness file)	6.0	3.2	100	300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	11000	630	.84	0	-					-					error (invalid witness file)	.50	.32	13	40	error (invalid witness file)	6.6	3.5	85	310
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	11000	1400	.84	0	-					-					error (invalid witness file)	.49	.32	6.8	43	error (invalid witness file)	6.3	3.3	120	300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9500	460	.99	0	-					-					error (invalid witness file)	.52	.34	6.8	39	error (invalid witness file)	5.9	3.1	85	300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9800	440	.84	0	-					-					error (invalid witness file)	.49	.32	11	39	error (invalid witness file)	6.5	3.5	110	300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9800	410	.84	0	-					-					error (invalid witness file)	.58	.38	7.7	43	error (invalid witness file)	5.4	2.9	99	290
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	10000	440	.99	0	-					-					error (invalid witness file)	.52	.34	7.0	40	error (invalid witness file)	5.9	3.1	110	290
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9500	1100	.99	0	-					-					error (invalid witness file)	.49	.31	7.6	41	error (invalid witness file)	5.9	3.2	100	300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	10000	770	.99	0	-					-					error (invalid witness file)	.48	.31	9.8	39	error (invalid witness file)	7.1	3.7	93	320
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	13000	250	.99	0	-					-					error (invalid witness file)	.49	.32	11	40	error (invalid witness file)	6.3	3.3	120	300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	5500	9200	.99	0	-					-					error (invalid witness file)	.51	.33	8.9	44	error (invalid witness file)	5.9	3.2	100	300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	8300	640	.99	0	-					-					error (invalid witness file)	.48	.31	8.4	39	error (invalid witness file)	6.6	3.5	93	310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	8600	1500	.84	0	-					-					error (invalid witness file)	.52	.35	5.6	41	error (invalid witness file)	5.7	3.1	89	300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	11000	400	.99	0	-					-					error (invalid witness file)	.54	.35	12	40	error (invalid witness file)	6.1	3.3	100	300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	13000	400	.99	0	-					-					error (invalid witness file)	.47	.29	4.8	39	error (invalid witness file)	5.8	3.1	83	310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9700	580	.99	0	-					-					error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	5.8	3.1	80	300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	11000	780	.99	0	-					-					error (invalid witness file)	.49	.32	6.7	40	error (invalid witness file)	5.8	3.1	72	300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i	timeout	0	wit	inspect	900	900	9800	1500	.99	0	-					-					error (invalid witness file)	.51	.33	12	40	error (invalid witness file)	6.0	3.2	94	300
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	.37	.37	4.1	30	.84	0	error (invalid witness file)	.52	.35	11	39	error (invalid witness file)	5.9	3.2	100	310	-					-
forester-heap/sll-01_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	.15	.15	2.7	25	.84	0	error (invalid witness file)	.51	.33	11	40	error (invalid witness file)	5.5	2.9	95	300	-					-
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i	false(valid-deref)	1	wit	inspect	.28	.28	3.3	25	.84	0	error (invalid witness file)	.53	.35	11	40	error (invalid witness file)	5.4	2.9	89	290	-					-
../../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	-31			31000	31000	350000	50000	48	0	52	13	8.3	270	1000	52	150	80	2400	7500	52	14	8.9	230	1100	52	170	88	2600	8200
correct results	17	17			1500	1500	17000	2300	15	0	0	8.8	5.7	180	670	0	100	53	1600	5100	0	0	0	0	0	0	0	0	0	0
correct true	0
correct false	17	17			1500	1500	17000	2300	15	0	0	8.8	5.7	180	670	0	100	53	1600	5100	0	0	0	0	0	0	0	0	0	0
correct-unconfimed results	0
correct-unconfirmed true	0
correct-unconfirmed false	0
incorrect results	3	-48			1100	1100	13000	2300	2.8	0	0	0	0	0	0	0	0	0	0	0	0	1.6	1.0	24	120	0	18	9.7	260	880
incorrect true	0
incorrect false	3	-48			1100	1100	13000	2300	2.8	0	0	0	0	0	0	0	0	0	0	0	0	1.6	1.0	24	120	0	18	9.7	260	880
score (52 tasks, max score: 79)	-31
Run set	sv-comp17.MemSafety-LinkedLists