Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 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 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.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 out of memory (false(no-overflow)) 0 wit inspect 720    15000 9100   error (recursion) 0 wit inspect 3.0 250 false(unreach-call) 1 wit inspect 6.9 280 unknown 0 wit inspect .93 51 error (1) 0 wit inspect .067 9.0 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 1.1  50 15   true -32 wit inspect 3.4 260 true -32 wit inspect 4.9 230 unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .88 49 12   true -32 wit inspect 3.2 260 true -32 wit inspect 4.8 230 unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .57 50 7.8 true -32 wit inspect 3.3 260 true -32 wit inspect 4.7 220 unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .58  18   - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 610    15000 7600   error (recursion) 0 wit inspect 3.1 250 false(unreach-call) 1 wit inspect 15   540 unknown 0 wit inspect 1.0  51 error (1) 0 wit inspect .067 9.0 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 610    15000 7000   error (recursion) 0 wit inspect 3.1 250 false(unreach-call) 1 wit inspect 22   860 unknown 0 wit inspect .92 53 error (1) 0 wit inspect .071 9.0 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .56 49 6.5 true -32 wit inspect 3.3 260 true -32 wit inspect 4.6 220 unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 720    15000 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 13   520
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 720    15000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9 250 true 2 wit inspect 26   740
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 720    15000 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 true 2 wit inspect 19   680
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 640    15000 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2 250 true 2 wit inspect 8.3 330
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout (false(no-overflow)) 0 wit inspect 900    15000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 420   4500
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 6.2  320 66   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 timeout 0 wit inspect 960   4700
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout (false(no-overflow)) 0 wit inspect 900    10000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 15   550
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 6.9  450 61   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 34   2900
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 610    15000 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3 250 true 2 wit inspect 37   3100
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 740    15000 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 240 true 2 wit inspect 7.9 280
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 710    15000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 timeout 0 wit inspect 960   1500
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory (false(no-overflow)) 0 wit inspect 710    15000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 timeout 0 wit inspect 960   4600
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 570    15000 7000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 true 2 wit inspect 8.9 360
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout (false(no-overflow)) 0 wit inspect 900    15000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2 250 timeout 0 wit inspect 960   1000
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 610    15000 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 timeout 0 wit inspect 960   5400
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 8.0  460 78   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 5.9 260
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 11    480 120   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 32   810
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  48 14   true -32 wit inspect 3.1 260 true -32 wit inspect 4.9 210 unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  48 13   true -32 wit inspect 3.0 250 true -32 wit inspect 3.0 210 unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .58  18   - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2  49 15   true -32 wit inspect 4.0 270 timeout 0 wit inspect 96   6600 unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .64  19   - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5  61 39   true -32 wit inspect 9.4 560 timeout 0 wit inspect 95   7000 unknown 0 wit inspect 6.9  410 false(unreach-call) 1 wit inspect 1.2   28   - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 19    520 260   true -32 wit inspect 44   2800 timeout 0 wit inspect 97   6900 unknown 0 wit inspect 39    2800 false(unreach-call) 1 wit inspect 7.2   130   - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 240    5400 3100   timeout 0 wit inspect 98   5000 out of memory 0 wit inspect 75   7000 timeout 0 wit inspect 98    4900 false(unreach-call) 1 wit inspect 75     1200   - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 1.3  49 15   true -32 wit inspect 3.9 270 true -32 wit inspect 36   2700 unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .64  20   - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 2.7  69 32   true -32 wit inspect 6.5 580 timeout 0 wit inspect 91   7000 unknown 0 wit inspect 7.2  520 false(unreach-call) 1 wit inspect 1.2   30   - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 20    610 240   true -32 wit inspect 54   3700 timeout 0 wit inspect 98   6900 unknown 0 wit inspect 56    3700 false(unreach-call) 1 wit inspect 7.4   170   - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 230    6400 3200   timeout 0 wit inspect 98   5300 out of memory 0 wit inspect 80   7000 timeout 0 wit inspect 98    5500 false(unreach-call) 1 wit inspect 77     1700   - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .39 48 4.7 true -32 wit inspect 3.1 260 true -32 wit inspect 4.7 230 unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  50 12   true -32 wit inspect 3.5 260 true -32 wit inspect 3.4 230 unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .58  18   - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2  49 13   true -32 wit inspect 3.5 260 true -32 wit inspect 5.3 240 unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2  50 14   true -32 wit inspect 3.3 260 true -32 wit inspect 5.3 300 unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .62  18   - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2  50 15   true -32 wit inspect 3.8 260 true -32 wit inspect 10   740 unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .60  19   - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 13   true -32 wit inspect 3.4 260 true -32 wit inspect 5.6 330 unknown 0 wit inspect 3.1  180 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 13   true -32 wit inspect 3.5 260 true -32 wit inspect 16   1100 unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .61  18   - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 1.1  49 12   true -32 wit inspect 3.2 250 true -32 wit inspect 4.7 220 unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .57  18   - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 16   true -32 wit inspect 3.5 270 true -32 wit inspect 5.1 230 unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 1.1  49 14   true -32 wit inspect 3.2 260 true -32 wit inspect 4.7 220 unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .58  18   - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  49 13   true -32 wit inspect 3.3 260 true -32 wit inspect 4.6 220 unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57  18   - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 12   true -32 wit inspect 3.3 260 true -32 wit inspect 5.1 240 unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 15   true -32 wit inspect 3.4 260 true -32 wit inspect 4.9 280 unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c unknown 0 wit inspect 5.1  300 48   true -32 wit inspect 3.6 280 true -32 wit inspect 4.6 250 unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .61  18   - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  49 14   true -32 wit inspect 3.4 260 true -32 wit inspect 4.7 220 unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 360    4300 3800   true -32 wit inspect 4.9 270 true -32 wit inspect 12   1100 unknown 0 wit inspect 4.1  220 true -32 wit inspect .70  29   - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 9.2  570 76   true -32 wit inspect 3.7 260 true -32 wit inspect 5.6 360 unknown 0 wit inspect 3.0  210 true -32 wit inspect .61  20   - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .93 49 11   true -32 wit inspect 2.3 260 true -32 wit inspect 5.1 220 unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .58  18   - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 12    690 110   true -32 wit inspect 4.0 270 true -32 wit inspect 6.3 480 unknown 0 wit inspect 3.4  220 true -32 wit inspect .63  21   - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .92 49 11   true -32 wit inspect 3.4 260 true -32 wit inspect 4.9 270 unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .90 49 10   true -32 wit inspect 3.2 260 true -32 wit inspect 4.7 210 unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  49 13   true -32 wit inspect 3.7 260 true -32 wit inspect 5.2 280 unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .59  18   - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 14   true -32 wit inspect 3.6 270 true -32 wit inspect 6.0 400 unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .59  19   - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.1  49 17   true -32 wit inspect 3.6 260 true -32 wit inspect 6.8 470 unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .65  19   - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c unknown 0 wit inspect 5.2  310 48   true -32 wit inspect 3.6 260 true -32 wit inspect 4.6 250 unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61  19   - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  49 12   true -32 wit inspect 3.3 250 true -32 wit inspect 4.6 230 unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58  18   - wit inspect - wit inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .39 49 4.4 true -32 wit inspect 3.3 260 true -32 wit inspect 4.5 230 unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60  18   - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 3.1  260 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1 250 true 2 wit inspect 5.0 260
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 3.0  260 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0 250 true 2 wit inspect 5.3 260
recursive-simple/fibo_10_true-unreach-call_true-termination.c unknown 0 wit inspect 8.1  500 74   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 56   4500
recursive-simple/fibo_15_true-unreach-call.c unknown 0 wit inspect 50    2400 640   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 timeout 0 wit inspect 960   5400
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 900    3900 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 timeout 0 wit inspect 960   6000
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 900    4400 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 timeout 0 wit inspect 960   6000
recursive-simple/fibo_2calls_10_true-unreach-call.c unknown 0 wit inspect 9.1  510 70   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6 250 true 2 wit inspect 84   4500
recursive-simple/fibo_2calls_15_true-unreach-call.c unknown 0 wit inspect 66    2200 810   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 240 timeout 0 wit inspect 960   5800
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900    3900 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9 250 timeout 0 wit inspect 960   5600
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900    4500 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7 250 timeout 0 wit inspect 960   6200
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 3.2  260 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0 250 true 2 wit inspect 9.1 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c unknown 0 wit inspect 4.9  300 45   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 15   540
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c unknown 0 wit inspect 5.1  300 48   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8 250 true 2 wit inspect 20   600
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c unknown 0 wit inspect 5.6  300 53   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7 250 true 2 wit inspect 28   760
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c unknown 0 wit inspect 6.2  360 58   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0 250 true 2 wit inspect 53   1600
recursive-simple/fibo_5_true-unreach-call_true-termination.c unknown 0 wit inspect 4.7  290 50   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 14   560
recursive-simple/fibo_7_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5  300 48   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 18   790
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.9  290 45   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6 250 true 2 wit inspect 11   430
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 5.0  300 48   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 11   470
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 5.1  300 52   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9 250 true 2 wit inspect 11   500
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c unknown 0 wit inspect 4.5  300 42   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 true 2 wit inspect 12   480
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.6  300 36   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0 250 true 2 wit inspect 9.5 360
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.6  290 44   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2 250 true 2 wit inspect 6.1 260
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.6  300 44   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8 250 true 2 wit inspect 6.2 260
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c unknown 0 wit inspect 4.8  300 44   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7 250 true 2 wit inspect 15   540
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c unknown 0 wit inspect 4.6  290 42   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3 250 true 2 wit inspect 20   630
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c unknown 0 wit inspect 4.8  300 50   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9 250 true 2 wit inspect 28   740
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c unknown 0 wit inspect 4.8  300 47   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 36   830
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c unknown 0 wit inspect 4.6  300 47   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9 250 true 2 wit inspect 10   430
recursive-simple/sum_10x0_true-unreach-call_true-termination.c unknown 0 wit inspect 4.8  300 41   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6 240 true 2 wit inspect 17   550
recursive-simple/sum_15x0_true-unreach-call_true-termination.c unknown 0 wit inspect 5.0  300 47   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3 250 true 2 wit inspect 23   700
recursive-simple/sum_20x0_true-unreach-call_true-termination.c unknown 0 wit inspect 5.3  300 49   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4 250 true 2 wit inspect 32   760
recursive-simple/sum_25x0_true-unreach-call_true-termination.c unknown 0 wit inspect 5.2  310 50   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 50   920
recursive-simple/sum_2x3_true-unreach-call_true-termination.c unknown 0 wit inspect 4.6  300 45   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 8.2 360
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 5.1  310 49   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9 250 true 2 wit inspect 13   300
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 42 16000   290000 210000 44 -1248 440 28000 44 -1085 900 64000 44 0 410 25000 44 -58 190   4000 52 6 170   13000 52 82 12000 92000
    correct results 39 42 560   15000 7300 0 3 3 44 1700 0 38 38 190   3900 3 6 9.2 740 41 82 1300 40000
        correct true 3 6 9.3 780 92 0 0 0 0 3 6 9.2 740 41 82 1300 40000
        correct false 36 36 550   15000 7300 0 3 3 44 1700 0 38 38 190   3900 0 0
    incorrect results 0 39 -1248 230 17000 34 -1088 220 14000 0 3 -96 1.9 70 0 0
        incorrect true 0 39 -1248 230 17000 34 -1088 220 14000 0 3 -96 1.9 70 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 42 -1248 -1085 0 -58 6 82
Run set depthk.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Recursive