Tool CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 3.4 290 32 0 91   1600 -32 7.5 270 0 2.7 180 -32 .59 18 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 3.4 290 31 1 3.3 270 1 5.3 250 0 3.4 230 -32 .63 18 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 3.1 280 29 -32 3.1 260 -32 5.2 230 0 3.6 180 -32 .57 18 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 3.5 290 27 1 3.4 260 1 6.9 260 0 3.6 180 1 .59 18 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 3.2 280 31 1 12   430 -32 10   310 0 2.2 210 -32 .62 18 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 1 3.4 280 28 1 35   490 -32 9.7 320 0 3.3 190 -32 .57 18 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 3.3 290 27 -32 3.6 270 -32 6.5 280 0 2.9 210 -32 .58 18 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c -16 3.4 280 31 - - - - 0 900   5300 2 8.5 350
recursive/Ackermann03_true-unreach-call_true-no-overflow.c -16 3.5 290 28 - - - - 0 16   350 2 7.1 280
recursive/Ackermann04_true-unreach-call_true-no-overflow.c -16 3.3 290 28 - - - - 0 86   1800 2 7.8 280
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c -16 3.4 280 27 - - - - 0 900   1400 2 9.3 360
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c -16 3.4 290 30 - - - - 0 900   4000 2 9.8 430
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c -16 3.4 290 30 - - - - 0 420   7000 2 22   630
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c -16 3.2 280 30 - - - - 0 900   1200 2 9.3 400
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c -16 3.3 290 32 - - - - 2 5.7 310 2 8.0 310
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c -16 3.2 280 32 - - - - 0 900   3700 2 9.7 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c -16 3.2 280 29 - - - - 2 3.8 280 2 7.0 280
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c -16 3.6 290 30 - - - - 0 900   1400 2 42   590
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c -16 3.8 290 32 - - - - 0 900   2300 2 15   520
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c -16 3.4 290 30 - - - - 2 4.6 280 2 8.3 290
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c -16 3.5 290 29 - - - - 0 900   750 2 98   1100
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c -16 3.4 290 33 - - - - 2 4.1 260 2 7.0 270
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c -16 3.3 280 30 - - - - 0 900   4100 2 5.6 260
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c -16 3.2 280 31 - - - - 0 790   7000 2 9.9 370
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 3.4 310 28 1 3.1 260 1 6.7 260 0 2.8 210 1 .61 18 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 3.1 270 29 1 3.5 280 1 6.8 260 0 3.6 180 1 .60 18 - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 1 3.2 280 28 1 5.2 340 -32 7.6 300 0 3.2 180 1 .58 18 - -
recursive-simple/fibo_15_false-unreach-call.c 1 3.2 280 26 1 13   1200 -32 10   310 0 3.5 190 1 .61 18 - -
recursive-simple/fibo_20_false-unreach-call.c 1 3.2 280 30 0 40   7000 -32 8.2 300 0 2.8 180 1 .59 18 - -
recursive-simple/fibo_25_false-unreach-call.c 1 3.3 280 28 0 96   4000 -32 8.3 300 0 3.1 210 1 .58 18 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 3.5 280 29 1 5.7 330 -32 17   500 0 3.2 180 1 .59 18 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 3.4 280 29 -32 3.7 260 -32 18   470 0 3.8 210 1 .58 18 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 1 3.4 290 31 0 39   7000 -32 16   530 0 3.1 190 1 .60 18 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 1 3.3 290 27 -32 3.9 260 -32 17   510 0 3.6 190 1 .61 18 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 3.6 280 32 1 3.0 260 1 6.0 250 0 3.9 210 1 .59 18 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 3.5 290 31 1 3.8 270 1 19   510 0 3.3 190 1 .58 18 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 3.6 280 33 -32 3.9 250 -32 16   510 0 3.3 180 1 .58 18 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 3.5 290 33 1 5.4 280 -32 14   500 0 3.5 210 1 .58 18 - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 1 3.4 290 32 1 4.8 290 -32 18   480 0 3.4 210 1 .62 18 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 3.2 280 32 1 3.6 270 -32 9.9 300 0 3.5 210 1 .58 18 - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 1 3.2 280 27 1 4.6 280 -32 8.8 310 0 3.2 190 1 .58 18 - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 3.4 290 30 1 3.8 280 1 5.2 260 0 2.8 180 -32 .58 18 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 3.4 280 30 1 4.2 270 1 10   360 0 3.4 190 1 .61 18 - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 3.3 280 26 1 3.5 260 1 7.2 260 0 2.7 180 -32 .58 18 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 3.1 280 26 1 3.8 270 -32 10   320 0 3.0 180 1 .61 18 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 3.2 280 27 1 3.8 270 -32 8.1 310 0 3.5 200 1 .58 18 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 3.2 280 31 1 3.7 270 -32 5.7 330 0 3.2 180 1 .57 18 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 3.1 280 32 1 4.0 270 -32 9.9 310 0 3.1 180 1 .60 18 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 3.3 280 30 1 3.6 270 -32 9.7 320 0 3.5 210 1 .58 18 - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 3.4 310 29 0 91   2400 -32 9.9 350 0 2.9 190 -32 .58 18 - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 1 3.1 280 31 1 9.4 490 -32 9.1 350 0 3.1 210 -32 .58 18 - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 1 3.1 280 28 1 3.9 270 -32 10   360 0 3.3 180 -32 .61 18 - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 1 3.6 310 31 1 22   930 -32 11   370 0 3.5 180 -32 .58 18 - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 1 3.2 280 31 1 4.8 280 -32 9.9 350 0 3.2 190 -32 .60 18 - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 1 3.2 280 27 1 3.7 260 1 6.7 270 0 3.1 180 -32 .58 19 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 3.2 280 27 1 3.8 270 -32 8.1 320 0 2.7 180 1 .61 18 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 3.2 280 31 1 4.4 270 -32 8.2 320 0 2.0 210 1 .59 18 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 3.2 280 28 1 4.2 280 -32 10   320 0 2.8 180 1 .59 18 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 3.1 280 30 1 4.9 280 -32 9.9 320 0 2.9 200 1 .60 18 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 3.2 280 30 1 3.8 260 1 6.3 260 0 3.4 190 1 .58 18 - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 1 3.1 280 29 1 3.2 260 1 5.1 270 0 3.5 190 1 .57 19 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 2.7 270 28 - - - - 2 3.9 260 2 6.2 260
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 2.8 270 24 - - - - 2 3.3 260 2 5.5 280
recursive-simple/fibo_10_true-unreach-call_true-termination.c -16 3.1 280 34 - - - - 2 6.8 400 2 9.8 310
recursive-simple/fibo_15_true-unreach-call.c -16 3.1 280 28 - - - - 2 38   1900 2 8.0 290
recursive-simple/fibo_20_true-unreach-call.c -16 3.2 280 29 - - - - 0 900   2100 2 8.6 310
recursive-simple/fibo_25_true-unreach-call.c -16 3.3 290 27 - - - - 0 930   2900 2 8.2 310
recursive-simple/fibo_2calls_10_true-unreach-call.c -16 3.5 290 30 - - - - 2 7.6 410 2 14   510
recursive-simple/fibo_2calls_15_true-unreach-call.c -16 3.4 290 30 - - - - 2 4.5 260 2 16   510
recursive-simple/fibo_2calls_20_true-unreach-call.c -16 3.5 280 34 - - - - 0 900   2000 2 18   520
recursive-simple/fibo_2calls_25_true-unreach-call.c -16 3.6 310 32 - - - - 2 3.9 260 2 9.3 500
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 2.9 270 26 - - - - 2 3.3 250 2 10   370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c -16 3.5 280 27 - - - - 2 4.4 260 2 19   520
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c -16 3.4 290 32 - - - - 2 4.1 260 2 15   520
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c -16 3.5 290 34 - - - - 2 4.6 260 2 16   510
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c -16 3.4 290 32 - - - - 2 5.4 270 2 14   500
recursive-simple/fibo_5_true-unreach-call_true-termination.c -16 3.1 280 28 - - - - 2 4.0 250 2 7.7 290
recursive-simple/fibo_7_true-unreach-call_true-termination.c -16 3.2 280 29 - - - - 2 4.1 260 2 9.1 290
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 2.9 270 25 - - - - 0 3.0 250 2 14   440
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 3.0 270 23 - - - - 0 3.0 250 2 13   500
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 2.9 270 29 - - - - 0 2.9 250 2 15   500
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c -16 3.2 280 31 - - - - 2 4.4 260 2 14   500
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 2.9 270 26 - - - - 0 3.6 250 2 8.8 350
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 2.8 270 27 - - - - 0 3.7 250 2 7.4 260
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 3.0 270 29 - - - - 0 3.4 250 2 8.4 330
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c -16 3.3 280 27 - - - - 2 3.8 260 2 9.1 320
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c -16 3.1 280 25 - - - - 2 3.6 260 2 10   310
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c -16 3.3 280 33 - - - - 2 4.5 260 2 8.3 320
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c -16 3.5 300 29 - - - - 2 4.9 260 2 8.6 320
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c -16 3.3 280 27 - - - - 2 4.1 270 2 9.5 320
recursive-simple/sum_10x0_true-unreach-call_true-termination.c -16 3.3 290 28 - - - - 2 4.9 260 2 9.2 330
recursive-simple/sum_15x0_true-unreach-call_true-termination.c -16 3.3 280 27 - - - - 2 4.1 260 2 11   330
recursive-simple/sum_20x0_true-unreach-call_true-termination.c -16 3.2 280 29 - - - - 2 4.3 270 2 10   330
recursive-simple/sum_25x0_true-unreach-call_true-termination.c -16 3.3 280 26 - - - - 2 4.6 260 2 10   330
recursive-simple/sum_2x3_true-unreach-call_true-termination.c -16 3.4 310 31 - - - - 2 3.4 270 2 8.4 340
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c -16 3.1 280 25 - - - - 2 4.7 270 2 11   290
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 96 -630 310 27000 2800 44 -126 580 35000 44 -1012 430 15000 44 0 140 8500 44 -418 26   810 52 60 12000 59000 52 104 670 20000
    correct results 49 58 160 14000 1400 34 34 210 12000 12 12 92 3500 0 30 30 18   550 30 60 170 9800 52 104 670 20000
        correct true 9 18 26 2500 240 0 0 0 0 30 60 170 9800 52 104 670 20000
        correct false 40 40 130 11000 1200 34 34 210 12000 12 12 92 3500 0 30 30 18   550 0 0
    correct-unconfimed results 4 0 13 1200 120 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 4 0 13 1200 120 0 0 0 0 0 0
    incorrect results 43 -688 140 12000 1300 5 -160 18 1300 32 -1024 340 11000 0 14 -448 8.2 260 0 0
        incorrect true 0 5 -160 18 1300 32 -1024 340 11000 0 14 -448 8.2 260 0 0
        incorrect false 43 -688 140 12000 1300 0 0 0 0 0 0
score (96 tasks, max score: 148) -630 -126 -1012 0 -418 60 104
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Recursive