cpa-seq.2017-01-13_0744.results.sv-comp17.Overflows-Other.xml.bz2.merged.xml.bz2

Tool	CPAchecker 1.6.1-svn 24048
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 07:44:08 CET [[ 2017-01-15 00:24:53 CET ]] [[ 2017-01-15 00:50:42 CET ]] [[ 2017-01-15 00:30:44 CET ]] [[ 2017-01-15 00:56:39 CET ]]
Run set	sv-comp17.Overflows-Other
Options	-sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.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)
recursive/Addition02WithOverflowBug_false-no-overflow.c	error (recursion)	0	wit	inspect	2.3	1.0	18	240	0	0	false(no-overflow)	3.3	1.9	42	250	false(no-overflow)	6.9	3.7	87	320	-					-
recursive/Addition03_false-no-overflow.c	error (recursion)	0	wit	inspect	2.3	1.0	22	240	0	0	false(no-overflow)	3.4	2.0	59	260	false(no-overflow)	7.1	3.8	110	320	-					-
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c	false(no-overflow)	1	wit	inspect	2.4	1.1	22	250	0	0	false(no-overflow)	3.8	2.1	76	260	false(no-overflow)	7.1	3.8	110	310	-					-
recursive/Ackermann01_true-unreach-call_true-no-overflow.c	error (recursion)	0	wit	inspect	2.3	1.1	20	240	0	0	-					-					error (recursion)	3.4	1.9	53	250	out of memory	460	340	6600	7000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.4	1.0	20	240	0	0	-					-					error (recursion)	3.5	2.0	67	250	out of memory	560	440	6600	7000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c	error (recursion)	0	wit	inspect	2.4	1.0	21	240	0	0	-					-					error (recursion)	3.4	1.9	56	250	out of memory	490	400	5300	7000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c	error (recursion)	0	wit	inspect	2.4	1.1	21	240	0	0	-					-					error (recursion)	3.4	1.9	55	240	out of memory	680	550	7400	7000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	21	240	0	0	-					-					error (recursion)	3.4	1.9	59	240	timeout	960	810	12000	4700
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	18	240	0	0	-					-					error (recursion)	3.5	2.0	73	250	timeout	960	810	13000	4700
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	19	240	0	0	-					-					error (recursion)	3.5	2.0	58	240	timeout	960	800	12000	4200
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	21	240	0	0	-					-					true	3.3	1.9	62	240	true	7.0	3.7	120	320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.4	1.0	19	250	0	0	-					-					error (recursion)	3.5	2.0	72	250	timeout	960	800	11000	4100
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	20	240	0	0	-					-					error (recursion)	3.4	1.9	60	250	timeout	960	800	11000	4100
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c	error (recursion)	0	wit	inspect	2.3	1.0	20	240	0	0	-					-					error (recursion)	3.4	1.9	76	250	timeout	960	890	14000	5800
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	18	240	0	0	-					-					error (recursion)	3.3	1.9	53	250	true	42	24	600	1200
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	19	250	0	0	-					-					error (recursion)	3.3	1.8	52	250	timeout	960	890	15000	5700
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.4	1.0	21	240	0	0	-					-					error (recursion)	3.3	1.9	54	240	timeout	960	890	20000	5800
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	21	240	0	0	-					-					error (recursion)	3.3	1.9	59	250	timeout	960	890	13000	5800
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.4	1.0	22	240	0	0	-					-					error (recursion)	3.2	1.8	51	240	true	9.7	5.3	150	360
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	19	250	0	0	-					-					error (recursion)	3.1	1.8	51	250	true	9.8	5.3	160	360
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.1	22	240	0	0	-					-					error (recursion)	3.4	1.9	56	240	timeout	960	840	12000	2000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c	error (recursion)	0	wit	inspect	2.5	1.1	26	250	0	0	-					-					error (recursion)	3.9	2.1	65	250	timeout	960	840	19000	2000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	20	240	0	0	-					-					error (recursion)	3.6	2.0	77	240	true	8.0	4.3	140	320
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.4	1.1	24	250	0	0	-					-					error (recursion)	3.5	2.0	60	240	true	18	9.9	260	490
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.4	1.0	21	240	0	0	-					-					false(no-overflow)	3.8	2.2	67	260	timeout	960	810	18000	4800
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	21	240	0	0	-					-					error (recursion)	3.1	1.8	50	250	timeout	960	800	14000	4200
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c	error (recursion)	0	wit	inspect	2.3	1.0	23	240	0	0	-					-					error (recursion)	3.3	1.9	57	250	timeout	960	790	11000	4300
bitvector/jain_1_false-no-overflow.i	false(no-overflow)	1	wit	inspect	2.4	1.1	22	240	0	0	false(no-overflow)	3.2	1.8	54	250	false(no-overflow)	7.1	3.8	140	310	-					-
bitvector/jain_2_false-no-overflow.i	false(no-overflow)	1	wit	inspect	2.3	1.0	22	250	0	0	false(no-overflow)	3.4	1.9	47	250	false(no-overflow)	7.4	3.9	86	310	-					-
bitvector/jain_4_false-no-overflow.i	false(no-overflow)	1	wit	inspect	2.4	1.1	19	240	0	0	false(no-overflow)	3.7	2.1	79	250	false(no-overflow)	7.4	4.0	160	310	-					-
bitvector/jain_5_false-no-overflow.i	timeout	0	wit	inspect	900	850	11000	1400	0	0	true	3.7	2.1	59	280	timeout	97	65	1800	1500	-					-
bitvector/jain_6_false-no-overflow.i	false(no-overflow)	1	wit	inspect	2.5	1.1	23	250	0	0	false(no-overflow)	3.5	2.0	67	250	false(no-overflow)	6.6	3.6	100	310	-					-
bitvector/jain_7_false-no-overflow.i	false(no-overflow)	1	wit	inspect	2.5	1.1	20	250	0	0	false(no-overflow)	3.5	2.0	58	260	false(no-overflow)	6.7	3.6	99	310	-					-
bitvector/modulus_false-no-overflow.i	false(no-overflow)	1	wit	inspect	2.8	1.1	27	280	0	0	false(no-overflow)	3.3	1.8	61	240	error (1)	7.0	3.7	75	310	-					-
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	23	6.3	180	590	0	0	-					-					true	12	6.1	170	360	true	8.3	4.5	180	330
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	21	6.1	170	570	0	0	-					-					true	11	6.0	140	350	true	8.7	4.7	160	330
bitvector/byte_add_false-unreach-call_true-no-overflow.i	true	2	wit	inspect	85	64	900	1400	0	0	-					-					true	17	8.8	170	600	true	7.8	4.2	150	320
bitvector/gcd_1_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	5.2	3.2	55	290	0	0	-					-					true	5.9	3.4	72	330	true	9.2	4.9	130	340
bitvector/gcd_2_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	74	69	700	440	0	0	-					-					true	5.2	2.9	110	300	true	7.9	4.3	140	320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	76	71	570	430	0	0	-					-					true	5.0	2.9	91	300	true	7.9	4.3	180	310
bitvector/gcd_4_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	2.9	1.2	25	250	0	0	-					-					true	4.7	2.6	100	280	true	13	7.2	230	440
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	4.1	1.6	36	260	0	0	-					-					true	4.8	2.6	97	290	true	8.3	4.4	160	330
bitvector/jain_1_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	910	880	7900	8800	0	0	-					-					true	4.2	2.3	74	280	true	7.0	3.7	140	310
bitvector/jain_2_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	910	890	8200	9500	0	0	-					-					true	4.2	2.3	72	270	true	7.2	3.8	130	320
bitvector/jain_4_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	910	890	9400	10000	0	0	-					-					true	4.8	2.7	94	280	true	6.6	3.5	120	300
bitvector/jain_5_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	900	850	11000	990	0	0	-					-					true	4.2	2.3	83	270	true	7.0	3.8	140	310
bitvector/jain_6_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	910	890	10000	10000	0	0	-					-					true	4.4	2.5	77	280	true	6.9	3.7	130	300
bitvector/jain_7_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	910	890	5300	5600	0	0	-					-					true	4.4	2.4	75	270	true	6.7	3.6	130	320
bitvector/modulus_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	900	860	9100	4200	0	0	-					-					true	5.6	3.0	88	290	error (1)	6.9	3.7	140	310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	3.1	1.3	28	260	0	0	-					-					true	4.7	2.6	81	280	true	7.4	4.0	160	320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	32	15	260	730	0	0	-					-					true	4.6	2.6	88	280	true	8.2	4.4	120	350
bitvector/parity_true-unreach-call_true-no-overflow.i	true	2	wit	inspect	16	4.4	110	430	0	0	-					-					true	5.1	2.8	91	280	true	7.2	3.8	130	320
bitvector/sum02_false-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	900	850	10000	1800	0	0	-					-					true	4.8	2.6	76	280	true	7.2	3.8	130	310
bitvector/sum02_true-unreach-call_true-no-overflow.i	timeout	0	wit	inspect	900	840	11000	1800	0	0	-					-					true	4.8	2.6	77	280	true	7.1	3.8	160	310
../../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	54	29			9500	9000	97000	68000	0	0	54	35	20	600	2500	54	160	99	2800	4300	54	200	110	3400	12000	54	16000	14000	220000	100000
correct results	18	29			360	250	3200	7400	0	0	7	24	14	440	1800	6	49	27	770	2200	11	80	43	1200	3700	11	94	51	1700	3700
correct true	11	22			340	240	3000	5600	0	0	0	0	0	0	0	0	0	0	0	0	11	80	43	1200	3700	11	94	51	1700	3700
correct false	7	7			17	7.5	150	1800	0	0	7	24	14	440	1800	6	49	27	770	2200	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 (54 tasks, max score: 98)	29
Run set	sv-comp17.Overflows-Other