Tool ULTIMATE Taipan 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 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-12-03 08:43:49 CET 2017-12-03 08:58:51 CET 2017-12-03 09:15:45 CET 2017-12-03 09:17:25 CET 2017-12-03 09:00:18 CET
Run set utaipan.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.NoOverflows-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0843.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/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0843.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
recursive/Addition02WithOverflowBug_false-no-overflow.c 1 4.1 230 36 1 3.5  270 1 5.3   260   0 .63   18    -
recursive/Addition03_false-no-overflow.c 1 4.1 240 39 1 3.6  260 1 4.9   250   0 .63   18    -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 1 4.8 290 39 1 3.2  260 1 5.6   260   -32 .62   18    -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 910   13000 5800 - - - 0 .044 5.0
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 910   13000 6500 - - - 0 .019 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 910   13000 6600 - - - 0 .022 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 910   13000 5400 - - - 0 .048 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900   4400 12000 - - - 0 .020 4.9
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 900   5100 12000 - - - 0 .048 5.0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900   2600 12000 - - - 0 .049 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 2 4.4 250 35 - - - 2 4.5   230  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 2 7.3 380 60 - - - 2 8.8   490  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 2 7.7 380 55 - - - 2 12     490  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 900   5000 12000 - - - 0 .023 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 900   13000 7200 - - - 0 .018 4.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 1 63   1500 490 - - - 0 960     5000  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 59   1500 450 - - - 0 960     5000  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 1 58   1600 440 - - - 0 960     5500  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 2 6.6 310 53 - - - 2 9.5   330  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 6.8 320 61 - - - 2 7.8   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 1 240   4800 2700 - - - 0 960     4000  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900   6800 12000 - - - 0 .019 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 5.7 300 49 - - - 2 6.1   270  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 2 32   820 270 - - - 2 13     500  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 910   13000 8900 - - - 0 .017 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 900   2700 11000 - - - 0 .038 4.9
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 900   2500 11000 - - - 0 .048 4.8
recursive-simple/id_b3_o2_false-no-overflow.c 1 4.5 280 40 1 3.4  260 1 5.7   270   -32 .62   18    -
recursive-simple/id_b3_o5_false-no-overflow.c 1 4.7 280 37 1 3.6  260 1 5.6   280   -32 .62   18    -
recursive-simple/id_b5_o10_false-no-overflow.c 1 4.7 280 39 1 3.5  260 1 5.0   260   -32 .60   18    -
recursive-simple/sum_non_eq_false-no-overflow.c 1 4.7 290 38 1 3.6  260 1 5.5   260   -32 .63   18    -
recursive-simple/sum_non_false-no-overflow.c 1 5.4 310 40 1 3.2  260 1 5.9   250   -32 .59   18    -
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 32 - - - 2 4.5   230  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 240 35 - - - 2 4.4   220  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 4.1 250 40 - - - 2 4.5   220  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 34 - - - 2 4.2   220  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 4.1 250 36 - - - 2 4.2   220  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 2 7.8 370 62 - - - 2 7.3   270  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 8.1 370 63 - - - 2 6.7   270  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 8.1 380 68 - - - 2 6.6   270  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 2 4.0 250 36 - - - 2 4.6   220  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 2 4.2 240 32 - - - 2 4.2   220  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 2 3.9 250 33 - - - 2 4.7   210  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 240 37 - - - 2 4.2   210  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 250 34 - - - 2 4.0   210  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 37 - - - 2 4.5   220  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 2 4.3 250 31 - - - 2 4.2   210  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 38 - - - 2 4.2   220  
bitvector/byte_add_1_false-no-overflow.i 0 110   4000 1100 0 .57 43 0 .020 5.0 0 .0017 .30 -
bitvector/byte_add_2_false-no-overflow.i 0 230   4600 2600 0 .57 41 0 .048 4.9 0 .0013 .26 -
bitvector/byte_add_false-no-overflow.i 0 160   2700 1800 0 .57 43 0 .038 4.8 0 .0015 .28 -
bitvector/jain_1_false-no-overflow.i 1 4.2 240 38 -32 3.1  260 1 4.6   230   1 .59   18    -
bitvector/jain_2_false-no-overflow.i 1 4.2 240 39 -32 3.1  260 1 4.8   230   1 .64   18    -
bitvector/jain_4_false-no-overflow.i 1 4.4 250 40 -32 3.3  260 1 4.8   230   1 .60   18    -
bitvector/jain_5_false-no-overflow.i 0 900   1500 13000 0 .57 41 0 .020 4.9 0 .0011 .34 -
bitvector/jain_6_false-no-overflow.i 1 4.4 250 38 -32 3.3  260 1 5.4   250   1 .63   18    -
bitvector/jain_7_false-no-overflow.i 1 4.4 250 37 -32 3.3  260 1 3.3   240   1 .59   18    -
bitvector/modulus_false-no-overflow.i 0 4.4 250 30 0 .56 41 0 .020 4.9 0 .0036 .29 -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 2 5.1 280 43 - - - 2 5.7   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 2 5.5 280 40 - - - 2 5.8   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 2 5.0 280 37 - - - 2 6.3   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 5.5 330 45 - - - 2 5.7   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 5.4 280 39 - - - 2 5.7   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 5.2 280 38 - - - 2 5.5   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 19   640 170 - - - 2 13     480  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 4.2 250 35 - - - 2 4.0   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2 4.2 250 35 - - - 2 4.5   210  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2 4.1 250 31 - - - 2 4.4   210  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2 3.9 230 32 - - - 2 4.1   210  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 2 4.2 250 34 - - - 2 4.1   220  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2 4.1 240 36 - - - 2 4.2   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2 4.0 240 33 - - - 2 3.9   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 4.3 250 34 - - - 0 .017 4.9
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 0 4.3 250 36 - - - 0 .018 4.9
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 4.0 240 33 - - - 0 .019 4.8
bitvector/parity_true-unreach-call_true-no-overflow.i 2 4.2 250 34 - - - 2 4.4   220  
bitvector/sum02_false-unreach-call_true-no-overflow.i 2 4.3 240 35 - - - 2 4.2   210  
bitvector/sum02_true-unreach-call_true-no-overflow.i 2 4.2 250 34 - - - 2 4.1   230  
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
total 78 97 14000 150000 150000 18 -152 47 3600 18 13 67 3300 18 -187 8.0 240 60 80 4100 30000
    correct results 53 93 300 15000 2500 8 8 28 2100 13 13 66 3300 5 5 3.1 92 40 80 230 10000
        correct true 40 80 240 12000 2000 0 0 0 40 80 230 10000
        correct false 13 13 59 3400 500 8 8 28 2100 13 13 66 3300 5 5 3.1 92 0
    correct-unconfimed results 4 4 420 9400 4100 0 0 0 0
        correct-unconfirmed true 4 4 420 9400 4100 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 5 -160 16 1300 0 6 -192 3.7 110 0
        incorrect true 0 5 -160 16 1300 0 6 -192 3.7 110 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 97 -152 13 -187 80
Run set utaipan.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.NoOverflows-Other