Tool ULTIMATE Automizer 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] 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-12-03 11:17:40 CET 2017-12-03 11:52:01 CET 2017-12-03 12:09:33 CET 2017-12-03 12:09:49 CET 2017-12-03 11:53:41 CET
Run set uautomizer.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.NoOverflows-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_1117.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/uautomizer.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_1117.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 6.0 330 42 1 4.1  260 1 4.9   250   0 .65   18    -
recursive/Addition03_false-no-overflow.c 1 4.4 240 35 1 3.3  260 1 5.3   250   0 .59   19    -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 1 4.8 290 44 1 3.2  260 1 5.5   260   -32 .60   18    -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 900   12000 10000 - - - 0 .018 4.9
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 900   13000 10000 - - - 0 .018 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 910   13000 9400 - - - 0 .020 4.9
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 910   13000 8200 - - - 0 .019 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900   5200 13000 - - - 0 .019 4.8
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 900   5200 12000 - - - 0 .018 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900   5200 11000 - - - 0 .018 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 2 4.2 240 34 - - - 2 4.1   230  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 2 10   520 90 - - - 2 12     480  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 2 11   510 98 - - - 2 12     490  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 900   5000 11000 - - - 0 .018 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 36   3800 410 - - - 2 43     3200  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 900   5400 11000 - - - 0 .018 4.9
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 900   5000 13000 - - - 0 .018 4.9
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 900   4800 11000 - - - 0 .018 4.8
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 2 6.8 310 53 - - - 2 7.5   270  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 6.5 310 54 - - - 2 7.7   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900   3100 12000 - - - 0 .020 5.0
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900   5000 14000 - - - 0 .018 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 5.7 300 47 - - - 2 6.2   270  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 2 11   530 100 - - - 2 13     490  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 900   4700 14000 - - - 0 .018 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 1 60   1500 600 - - - 0 960     2900  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 1 57   1700 520 - - - 0 960     2700  
recursive-simple/id_b3_o2_false-no-overflow.c 1 4.6 290 37 1 3.5  260 1 5.1   260   -32 .63   18    -
recursive-simple/id_b3_o5_false-no-overflow.c 1 4.8 280 35 1 3.4  260 1 5.3   260   -32 .59   18    -
recursive-simple/id_b5_o10_false-no-overflow.c 1 4.7 280 39 1 3.3  260 1 5.4   260   -32 .59   19    -
recursive-simple/sum_non_eq_false-no-overflow.c 1 4.8 280 40 1 3.4  260 1 5.8   250   -32 .63   18    -
recursive-simple/sum_non_false-no-overflow.c 1 5.2 300 46 1 3.0  250 1 5.7   260   -32 .63   18    -
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 38 - - - 2 3.9   220  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 34 - - - 2 4.2   220  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 4.0 240 33 - - - 2 4.3   220  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 4.1 250 39 - - - 2 4.3   220  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 4.0 230 35 - - - 2 4.4   220  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 2 6.2 310 53 - - - 2 6.7   270  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 6.0 310 52 - - - 2 6.7   270  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 5.9 300 55 - - - 2 6.8   270  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 250 35 - - - 2 4.3   210  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 2 4.3 240 35 - - - 2 4.3   210  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 240 38 - - - 2 3.9   210  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 240 37 - - - 2 4.0   210  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 2 4.1 240 34 - - - 2 4.0   210  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 2 4.2 250 35 - - - 2 4.0   210  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 2 3.8 240 34 - - - 2 5.3   280  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 3.9 240 32 - - - 2 4.2   210  
bitvector/byte_add_1_false-no-overflow.i 0 25   650 250 0 .53 41 0 .046 4.9 0 .0047 .26 -
bitvector/byte_add_2_false-no-overflow.i 0 38   800 370 0 .53 41 0 .049 4.8 0 .0023 .28 -
bitvector/byte_add_false-no-overflow.i 0 69   810 790 0 .50 41 0 .026 5.0 0 .0037 .33 -
bitvector/jain_1_false-no-overflow.i 1 4.2 250 37 -32 3.0  260 1 4.6   230   1 .63   19    -
bitvector/jain_2_false-no-overflow.i 1 4.1 240 34 -32 3.2  260 1 5.0   230   1 .61   18    -
bitvector/jain_4_false-no-overflow.i 1 4.2 240 33 -32 3.3  260 1 5.1   240   1 .63   18    -
bitvector/jain_5_false-no-overflow.i 0 900   5200 12000 0 .53 43 0 .025 4.8 0 .0038 .32 -
bitvector/jain_6_false-no-overflow.i 1 4.3 250 37 -32 3.3  260 1 5.0   230   1 .61   18    -
bitvector/jain_7_false-no-overflow.i 1 4.2 250 35 -32 3.3  260 1 5.0   260   1 .64   18    -
bitvector/modulus_false-no-overflow.i 0 4.2 240 36 0 .54 41 0 .026 4.8 0 .0012 .35 -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 2 5.0 280 41 - - - 2 6.0   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 2 5.5 290 45 - - - 2 5.8   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 2 5.1 290 41 - - - 2 6.0   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 5.5 310 44 - - - 2 5.7   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 5.5 290 46 - - - 2 5.7   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 5.3 290 44 - - - 2 5.5   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 11   540 92 - - - 2 14     490  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 4.3 250 34 - - - 2 4.6   220  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2 4.2 250 35 - - - 2 3.9   220  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2 6.6 340 48 - - - 2 4.0   220  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2 4.0 240 33 - - - 2 4.1   220  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 2 4.2 250 40 - - - 2 4.3   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2 4.1 240 34 - - - 2 4.1   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2 4.0 240 32 - - - 2 3.9   210  
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 4.3 240 36 - - - 0 .019 4.9
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 0 4.2 250 35 - - - 0 .019 5.0
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 4.5 250 32 - - - 0 .018 4.9
bitvector/parity_true-unreach-call_true-no-overflow.i 2 4.3 250 35 - - - 2 4.3   220  
bitvector/sum02_false-unreach-call_true-no-overflow.i 2 4.1 240 33 - - - 2 4.0   210  
bitvector/sum02_true-unreach-call_true-no-overflow.i 2 4.1 240 34 - - - 2 4.1   220  
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 130000 180000 18 -152 46 3600 18 13 68 3300 18 -187 8.0 240 60 82 2200 19000
    correct results 54 95 310 19000 2700 8 8 27 2100 13 13 68 3200 5 5 3.1 92 41 82 270 14000
        correct true 41 82 250 15000 2200 0 0 0 41 82 270 14000
        correct false 13 13 60 3500 490 8 8 27 2100 13 13 68 3200 5 5 3.1 92 0
    correct-unconfimed results 2 2 120 3200 1100 0 0 0 0
        correct-unconfirmed true 2 2 120 3200 1100 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 82
Run set uautomizer.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.NoOverflows-Other