Tool ULTIMATE Automizer 0.1.23-3204b741 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-12-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Recursive
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.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 1 6.2 300 51 1 11    450 1 6.2   310   0 3.7  220 -32 .77   19    - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 5.6 300 47 1 2.6  270 1 5.3   260   0 3.8  190 0 .76   18    - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 1 5.5 290 40 -32 3.0  260 1 5.2   260   0 3.5  180 -32 .73   18    - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 4.3 250 33 1 3.0  260 1 5.0   250   0 3.1  180 1 .74   18    - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 10   560 86 1 47    1200 1 13     640   0 4.5  220 -32 .78   18    - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 18   1100 170 0 91    2500 0 97     4800   0 37    1800 -32 .64   20    - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 4.2 240 31 1 3.1  260 1 5.0   260   0 2.9  210 -32 .74   18    - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 2 12   530 86 - - - - 0 3.0  250 2 16     500  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 2 33   1100 280 - - - - 0 3.6  250 2 31     780  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 2 18   770 180 - - - - 0 3.8  250 2 25     690  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 2 6.8 340 61 - - - - 0 3.1  250 2 8.5   330  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 2 340   4600 4300 - - - - 0 3.9  250 2 440     4500  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900   3900 13000 - - - - 0 .56 43 0 .022 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 2 10   540 94 - - - - 0 3.9  250 2 18     540  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 40   3300 430 - - - - 0 3.2  250 2 33     2700  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 2 43   3400 360 - - - - 0 3.3  250 2 37     3200  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 6.3 320 54 - - - - 0 3.0  250 2 9.1   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900   1400 11000 - - - - 0 .62 41 0 .020 5.0
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900   4900 13000 - - - - 0 .61 43 0 .020 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 7.5 370 60 - - - - 0 3.4  250 2 9.3   350  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900   1200 12000 - - - - 0 .70 42 0 .019 5.0
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 900   5500 11000 - - - - 0 .53 41 0 .022 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2 4.9 290 42 - - - - 0 3.7  250 2 5.5   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 2 26   820 300 - - - - 0 3.5  250 2 34     780  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 4.7 290 43 -32 2.8  250 1 4.7   240   0 3.1  210 1 .71   18    - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 4.2 240 40 -32 3.2  260 1 5.2   270   0 2.8  210 1 .62   18    - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 1 31   2700 260 0 97    2900 0 97     6500   0 92    2900 1 .81   22    - -
recursive-simple/fibo_15_false-unreach-call.c 0 900   5600 12000 0 .47 44 0 .018 4.8 0 .86 50 0 .0017 .29 - -
recursive-simple/fibo_20_false-unreach-call.c 0 900   5600 11000 0 .63 43 0 .020 4.9 0 .89 47 0 .0013 .27 - -
recursive-simple/fibo_25_false-unreach-call.c 0 900   5600 11000 0 .63 44 0 .020 4.9 0 1.1  52 0 .0016 .29 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 73   4600 730 0 7.5  280 0 96     5700   0 5.1  220 1 .86   23    - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 900   5900 14000 0 .71 43 0 .020 4.9 0 .94 49 0 .0019 .28 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 900   6700 11000 0 .57 45 0 .019 4.8 0 .81 49 0 .0014 .28 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 900   5900 12000 0 .55 41 0 .019 4.9 0 .99 49 0 .0012 .30 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 6.0 290 47 1 3.6  260 1 5.0   260   0 3.0  180 1 .70   18    - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 9.7 550 69 1 7.1  350 1 7.3   330   0 3.8  220 1 .61   19    - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 13   600 110 1 10    470 1 39     950   0 6.2  260 1 .75   19    - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 14   670 130 1 29    870 1 56     2400   0 9.3  420 1 .60   19    - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 1 32   1600 280 0 92    2900 0 97     4000   0 66    2600 1 .66   20    - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 10   590 86 1 11    320 1 20     660   0 4.6  220 1 .72   18    - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 1 14   670 120 1 38    1700 1 61     1900   0 15    500 1 .77   19    - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 5.9 300 47 1 4.7  260 1 5.1   250   0 3.0  200 -32 .78   18    - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 7.6 390 66 1 4.1  260 1 4.3   260   0 3.2  180 1 .81   18    - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 5.8 310 47 1 4.9  260 1 3.8   240   0 2.8  180 -32 .69   18    - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 10   570 88 1 3.7  270 -32 3.0   230   0 3.2  230 1 .79   19    - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 15   660 140 1 4.8  270 -32 5.6   230   0 3.8  210 1 .61   19    - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 23   800 230 1 6.4  280 -32 5.3   250   0 4.2  210 1 .68   19    - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 27   860 300 1 6.1  270 -32 5.6   240   0 4.6  220 1 .64   18    - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 6.7 340 54 1 3.9  260 1 3.7   260   0 3.8  180 1 .75   18    - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 900   690 10000 0 .65 41 0 .020 4.8 0 1.1  49 0 .0012 .34 - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 0 900   700 12000 0 .54 42 0 .020 5.0 0 .90 50 0 .0013 .27 - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 1 11   540 98 1 4.5  270 -32 5.0   220   0 3.2  210 -32 .59   19    - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 0 900   800 12000 0 .63 41 0 .020 4.9 0 .93 49 0 .0015 .28 - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 1 290   710 4100 1 4.6  270 -32 4.7   230   0 4.5  220 -32 .67   19    - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 1 6.1 300 47 1 3.3  260 1 6.4   240   0 2.9  180 -32 .61   18    - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 10   540 90 1 3.9  270 -32 3.3   230   0 3.6  210 1 .77   18    - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 15   670 120 1 4.2  270 -32 5.0   240   0 3.9  190 1 .78   19    - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 18   800 140 1 4.9  270 -32 5.7   260   0 4.3  210 1 .75   19    - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 25   910 220 1 6.3  280 -32 5.2   260   0 3.1  210 1 .64   19    - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 5.6 290 41 1 3.3  260 1 3.8   250   0 3.7  190 1 .58   18    - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 1 4.2 240 34 1 3.3  260 1 6.1   250   0 3.6  210 1 .62   18    - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 4.6 280 39 - - - - 2 3.5  250 2 5.9   260  
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 4.5 290 40 - - - - 2 3.8  250 2 5.0   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c 2 70   4600 720 - - - - 0 3.8  250 2 53     4500  
recursive-simple/fibo_15_true-unreach-call.c 0 900   5400 12000 - - - - 0 .67 41 0 .024 4.8
recursive-simple/fibo_20_true-unreach-call.c 0 900   5700 11000 - - - - 0 .69 44 0 .020 4.8
recursive-simple/fibo_25_true-unreach-call.c 0 900   5700 11000 - - - - 0 .63 41 0 .018 4.9
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 110   4600 1100 - - - - 0 3.3  250 2 120     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c 0 900   6000 11000 - - - - 0 .66 41 0 .019 4.8
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 900   5700 12000 - - - - 0 .40 43 0 .019 4.9
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 900   6100 10000 - - - - 0 .55 43 0 .019 4.9
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 7.7 400 63 - - - - 2 4.1  270 2 9.7   360  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 13   630 120 - - - - 0 3.2  250 2 16     540  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 17   710 140 - - - - 0 2.2  250 2 22     660  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 24   850 190 - - - - 0 3.8  250 2 28     750  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 47   2100 420 - - - - 0 3.1  250 2 46     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 13   640 120 - - - - 0 3.1  250 2 16     550  
recursive-simple/fibo_7_true-unreach-call_true-termination.c 2 18   950 170 - - - - 0 3.0  250 2 22     810  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 8.4 440 67 - - - - 0 3.1  250 2 7.3   430  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 9.3 520 72 - - - - 0 4.1  250 2 11     480  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 9.2 520 82 - - - - 0 3.9  250 2 12     490  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 9.7 560 71 - - - - 0 4.0  250 2 13     480  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 7.1 350 59 - - - - 0 3.6  250 2 8.6   350  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 5.7 300 45 - - - - 0 3.1  250 2 6.5   260  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 6.0 300 55 - - - - 0 3.7  250 2 7.6   270  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 11   590 100 - - - - 0 3.6  250 2 15     530  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 15   660 130 - - - - 0 2.3  250 2 19     630  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 20   750 200 - - - - 0 3.5  250 2 30     740  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 27   920 220 - - - - 0 2.6  250 2 36     820  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 8.2 450 65 - - - - 0 3.1  250 2 11     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 13   620 100 - - - - 0 4.1  250 2 17     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 17   690 130 - - - - 0 2.9  250 2 23     690  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 23   840 190 - - - - 0 3.6  250 2 33     720  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 32   1000 350 - - - - 0 4.0  260 2 44     930  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 7.4 380 67 - - - - 0 2.9  250 2 8.7   350  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 8.5 320 89 - - - - 0 2.6  250 2 13     310  
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 116 20000 160000 250000 44 -68 540   21000 44 -299 710 34000 44 0 340 15000 44 -296 25   660 52 6 150 11000 52 82 1300 39000
    correct results 75 116 1800 67000 20000 28 28 240   11000 21 21 270 11000 0 24 24 17   450 3 6 11 770 41 82 1300 39000
        correct true 41 82 1100 43000 12000 0 0 0 0 3 6 11 770 41 82 1300 39000
        correct false 34 34 740 24000 8100 28 28 240   11000 21 21 270 11000 0 24 24 17   450 0 0
    correct-unconfimed results 1 0 18 1100 170 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 18 1100 170 0 0 0 0 0 0
    incorrect results 0 3 -96 9.0 760 10 -320 48 2400 0 10 -320 7.0 190 0 0
        incorrect true 0 3 -96 9.0 760 10 -320 48 2400 0 10 -320 7.0 190 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 116 -68 -299 0 -296 6 82
Run set uautomizer.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Recursive