Tool DepthK 3.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 09:26:28 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 280    260    15000 3300   31    0      error (recursion) 0 wit inspect 3.7 2.2 250 0   0   false(unreach-call) 1 --- inspect 10   6.2 330 .62 0   unknown 0 --- inspect .99 .64 50 0   0   error (1) 0 --- inspect .078 .078 11 0     0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .40 .39 34 4.8 31    0      false(unreach-call) 1 wit inspect 5.3 3.0 270 0   0   true -32 --- inspect 8.3 5.2 310 .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .57  .58  20 .049 0      - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .37 .36 35 4.5 31    0      true -32 wit inspect 3.8 2.2 250 0   0   true -32 --- inspect 7.0 4.4 310 .66 0   unknown 0 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .57  .58  20 .049 .0041 - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .16 .16 34 1.7 1.0  0      false(unreach-call) 1 wit inspect 4.4 2.4 250 0   0   false(unreach-call) 1 --- inspect 6.8 4.0 300 .62 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .58  .58  20 .049 .0041 - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    200    15000 2800   31    0      error (recursion) 0 wit inspect 4.2 2.4 250 0   0   false(unreach-call) 1 --- inspect 15   8.9 500 .62 0   unknown 0 --- inspect .97 .63 50 0   0   error (1) 0 --- inspect .068 .069 12 0     .0041 - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    200    15000 2500   26    0      error (recursion) 0 wit inspect 3.7 2.1 250 0   0   false(unreach-call) 1 --- inspect 29   17   960 .62 0   unknown 0 --- inspect .97 .63 49 0   0   error (1) 0 --- inspect .072 .073 11 0     0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .13 .13 33 1.9 1.0  0      false(unreach-call) 1 wit inspect 3.7 2.0 250 0   0   false(unreach-call) 1 --- inspect 8.3 4.6 310 .62 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 270    260    15000 3300   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0 2.2 250 0   0   true 2 --- inspect 19   11   470 .62 0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 270    260    15000 3800   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.8 2.7 250 0   0   true 2 --- inspect 33   21   750 .62 0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 280    260    15000 3800   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9 2.2 250 0   0   true 2 --- inspect 23   14   670 .62 0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 260    250    15000 3600   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2 2.3 250 0   0   true 2 --- inspect 12   6.7 380 .66 0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 260    250    15000 3400   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.1 250 0   0   true 2 --- inspect 420   330   2300 .62 0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .87 .61 67 9.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   timeout 0 --- inspect 960   810   1400 .63 0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 220    200    15000 3200   26    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.1 250 0   0   true 2 --- inspect 18   11   560 .62 0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .82 .54 66 8.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 39   24   1600 .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    200    15000 2600   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 37   23   1400 .62 0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 200    200    15000 3000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 10   5.8 340 .66 0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 240    230    15000 3500   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   timeout 0 --- inspect 960   820   1100 .64 0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 250    230    15000 3000   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0 2.2 250 0   0   timeout 0 --- inspect 960   820   1200 .65 0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 270    260    15000 3600   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.1 250 0   0   true 2 --- inspect 11   6.6 360 .66 0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 270    260    15000 3600   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.0 250 0   0   timeout 0 --- inspect 960   830   910 .64 0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 280    270    15000 4300   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8 2.2 250 0   0   timeout 0 --- inspect 960   900   6000 .63 0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .78 .54 67 9.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.1 250 0   0   true 2 --- inspect 8.5 4.8 310 .42 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .87 .59 66 9.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.0 250 0   0   true 2 --- inspect 15   9.1 510 .66 0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 .37 34 4.2 31    0      false(unreach-call) 1 wit inspect 3.8 2.1 250 0   0   true -32 --- inspect 6.4 4.1 290 .66 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .58  .58  20 .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32 .32 34 4.1 26    0      false(unreach-call) 1 wit inspect 3.7 2.1 250 0   0   true -32 --- inspect 7.7 4.4 310 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .56  .56  20 .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 .33 35 4.1 31    0      false(unreach-call) 1 wit inspect 8.2 4.6 330 0   0   true -32 --- inspect 9.0 5.0 310 .62 0   false(unreach-call) 1 --- inspect 3.3  1.9  250 0   0   false(unreach-call) 1 --- inspect .59  .59  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .47 .46 34 7.1 31    0      false(unreach-call) 1 wit inspect 22   14   1200 0   0   true -32 --- inspect 7.2 4.6 310 .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 2.1  2.0  100 31   33    0      out of memory 0 --- inspect 46   35   7000 0   0   true -32 --- inspect 7.6 4.8 310 .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .58  .59  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 21    20    950 310   53    0      timeout 0 --- inspect 97   63   3600 0   0   true -32 --- inspect 7.4 4.7 310 .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .59  .59  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .36 .36 34 3.9 31    0      false(unreach-call) 1 wit inspect 7.8 4.3 330 0   0   true -32 --- inspect 7.5 4.3 300 .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .48 .47 35 5.6 31    0      false(unreach-call) 1 wit inspect 25   16   1200 0   0   true -32 --- inspect 8.1 5.0 310 .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .58  .58  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 2.1  2.0  100 28   33    0      out of memory 0 --- inspect 47   36   7000 0   0   true -32 --- inspect 7.9 4.5 310 .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 22    21    950 330   53    0      timeout 0 --- inspect 97   60   3600 0   0   true -32 --- inspect 7.6 4.3 310 .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .58  .58  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 .13 33 1.8 1.0  0      false(unreach-call) 1 wit inspect 4.0 2.2 250 0   0   true -32 --- inspect 8.0 4.5 310 .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .61  .60  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 .34 35 4.1 26    0      false(unreach-call) 1 wit inspect 4.5 2.5 260 0   0   true -32 --- inspect 7.6 4.3 300 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .58  .58  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 .35 34 3.7 31    0      false(unreach-call) 1 wit inspect 5.2 2.9 270 0   0   true -32 --- inspect 8.0 4.6 310 .66 0   false(unreach-call) 1 --- inspect 4.2  2.5  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .33 35 4.7 31    0      false(unreach-call) 1 wit inspect 4.7 2.6 270 0   0   true -32 --- inspect 7.7 4.4 310 .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .61  .60  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 .33 34 3.7 26    0      false(unreach-call) 1 wit inspect 6.0 3.3 280 0   0   true -32 --- inspect 7.6 4.4 310 .62 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0   false(unreach-call) 1 --- inspect .60  .60  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .33 34 4.6 31    0      false(unreach-call) 1 wit inspect 4.7 2.6 260 0   0   true -32 --- inspect 7.7 4.4 310 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 .34 34 4.4 31    0      false(unreach-call) 1 wit inspect 4.9 2.7 280 0   0   true -32 --- inspect 7.6 4.3 310 .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0   false(unreach-call) 1 --- inspect .58  .58  20 .049 .0041 - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .34 .33 34 4.0 31    0      false(unreach-call) 1 wit inspect 6.0 3.3 270 0   0   false(unreach-call) 1 --- inspect 8.2 4.6 310 .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .59  .59  20 .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .32 35 3.8 31    0      false(unreach-call) 1 wit inspect 5.2 2.9 260 0   0   true -32 --- inspect 7.1 4.1 300 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .60  .60  20 .049 .0041 - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .49 .48 36 6.8 31    0      false(unreach-call) 1 wit inspect 5.3 2.9 260 0   0   false(unreach-call) 1 --- inspect 11   6.3 320 .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .60  .61  20 .049 0      - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .33 35 4.1 31    0      false(unreach-call) 1 wit inspect 4.9 2.7 260 0   0   true -32 --- inspect 7.3 4.3 310 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .56  .56  20 .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 .33 34 4.8 31    0      false(unreach-call) 1 wit inspect 4.8 2.7 270 0   0   true -32 --- inspect 7.7 4.3 310 .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .56  .57  20 .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .33 35 4.2 31    0      false(unreach-call) 1 wit inspect 4.5 2.5 270 0   0   true -32 --- inspect 7.5 4.3 310 .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57  .59  20 .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c unknown 0 wit inspect .80 .55 67 8.5 31    0      error (recursion) 0 wit inspect 4.1 2.3 250 0   0   false(unreach-call) 1 --- inspect 39   27   660 .62 0   unknown 0 --- inspect .98 .64 49 0   0   error (1) 0 --- inspect .070 .070 11 0     0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 .35 34 4.8 31    0      false(unreach-call) 1 wit inspect 4.1 2.3 260 0   0   true -32 --- inspect 7.5 4.2 320 .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .59  .59  20 .045 .0041 - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .81 .55 66 8.2 31    0      error (recursion) 0 wit inspect 3.5 2.0 250 0   0   timeout 0 --- inspect 97   85   730 1.7  0   unknown 0 --- inspect .97 .63 50 0   0   error (1) 0 --- inspect .074 .075 11 0     .0041 - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .78 .53 65 9.0 31    0      error (recursion) 0 wit inspect 4.2 2.4 250 0   0   timeout 0 --- inspect 97   86   680 1.5  0   unknown 0 --- inspect 1.0  .65 50 0   0   error (1) 0 --- inspect .068 .067 11 0     0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .33 .32 34 4.1 31    0      false(unreach-call) 1 wit inspect 6.2 3.5 280 0   0   true -32 --- inspect 9.3 5.8 320 .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57  .59  20 .049 .0041 - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .81 .55 66 9.1 31    0      error (recursion) 0 wit inspect 3.7 2.1 250 0   0   timeout 0 --- inspect 97   86   700 1.5  0   unknown 0 --- inspect 1.0  .67 50 0   0   error (1) 0 --- inspect .10  .098 11 0     0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .34 .33 35 4.9 31    0      false(unreach-call) 1 wit inspect 9.5 5.2 420 0   0   true -32 --- inspect 8.0 4.6 310 .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .33 .33 35 3.8 31    0      false(unreach-call) 1 wit inspect 4.8 2.7 270 0   0   true -32 --- inspect 8.2 5.2 310 .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .61  .60  20 .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .33 34 4.6 31    0      false(unreach-call) 1 wit inspect 5.4 3.0 260 0   0   true -32 --- inspect 7.2 4.6 310 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .56  .56  20 .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 .35 35 4.9 31    0      false(unreach-call) 1 wit inspect 4.5 2.5 270 0   0   true -32 --- inspect 7.9 4.4 320 .66 0   false(unreach-call) 1 --- inspect 3.3  1.9  250 0   0   false(unreach-call) 1 --- inspect .60  .60  20 .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .32 35 4.4 31    0      false(unreach-call) 1 wit inspect 4.9 2.7 270 0   0   true -32 --- inspect 7.5 4.2 310 .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .56  .56  20 .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c unknown 0 wit inspect .83 .56 67 8.8 30    0      error (recursion) 0 wit inspect 4.2 2.3 250 0   0   false(unreach-call) 1 --- inspect 31   20   600 .62 0   unknown 0 --- inspect .99 .65 49 0   0   error (1) 0 --- inspect .077 .076 11 0     0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 .33 34 5.7 26    .0041 false(unreach-call) 1 wit inspect 4.2 2.3 260 0   0   true -32 --- inspect 7.3 4.2 310 .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .045 0      - --- inspect - --- inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .14 .13 33 1.5 .85 0      false(unreach-call) 1 wit inspect 3.7 2.1 250 0   0   false(unreach-call) 1 --- inspect 6.6 4.3 310 .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .57  .57  20 .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c unknown 0 wit inspect .81 .54 66 8.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6 2.1 250 0   0   true 2 --- inspect 7.4 4.6 310 .66 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c unknown 0 wit inspect .81 .53 67 8.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0 2.2 250 0   0   true 2 --- inspect 7.4 4.2 310 .66 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .54 66 7.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.1 250 0   0   true 2 --- inspect 37   23   2000 .62 0  
recursive-simple/fibo_15_true-unreach-call.c unknown 0 wit inspect .92 .66 67 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1 2.3 250 0   0   timeout 0 --- inspect 960   900   5900 .63 0  
recursive-simple/fibo_20_true-unreach-call.c unknown 0 wit inspect 2.5  2.2  100 33   27    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2 2.3 250 0   0   timeout 0 --- inspect 960   920   4900 1.0  0  
recursive-simple/fibo_25_true-unreach-call.c unknown 0 wit inspect 22    21    950 290   53    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.1 250 0   0   timeout 0 --- inspect 960   910   5800 .63 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c unknown 0 wit inspect .80 .54 66 8.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.0 250 0   0   true 2 --- inspect 110   68   3500 .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c unknown 0 wit inspect .95 .68 66 9.6 26    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   timeout 0 --- inspect 960   900   5300 .63 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c unknown 0 wit inspect 2.5  2.2  100 32   33    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0 2.3 250 0   0   timeout 0 --- inspect 960   910   5700 .63 0  
recursive-simple/fibo_2calls_25_true-unreach-call.c unknown 0 wit inspect 22    21    950 320   53    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.1 250 0   0   timeout 0 --- inspect 960   900   5100 .63 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c unknown 0 wit inspect .82 .55 67 8.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7 2.1 250 0   0   true 2 --- inspect 12   6.9 400 .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c unknown 0 wit inspect .85 .57 67 9.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.0 250 0   0   true 2 --- inspect 18   11   550 .62 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c unknown 0 wit inspect .81 .55 66 9.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 24   15   500 .62 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c unknown 0 wit inspect .82 .55 67 10   26    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2 2.3 250 0   0   true 2 --- inspect 29   18   720 .62 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .54 66 8.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0 2.2 250 0   0   true 2 --- inspect 44   28   1100 .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c unknown 0 wit inspect .85 .58 66 8.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4 1.9 250 0   0   true 2 --- inspect 16   9.7 510 .62 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c unknown 0 wit inspect .82 .55 67 9.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9 2.2 250 0   0   true 2 --- inspect 24   15   670 .62 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .84 .58 66 9.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 13   7.6 450 .62 0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .83 .57 68 8.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4 1.9 250 0   0   true 2 --- inspect 18   11   500 .62 0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .81 .56 66 9.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.0 250 0   0   true 2 --- inspect 18   11   460 .66 0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .54 66 8.9 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1 2.3 250 0   0   true 2 --- inspect 14   8.5 450 .62 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .82 .57 67 8.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4 1.9 260 0   0   true 2 --- inspect 12   7.1 390 .62 0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .93 .66 68 9.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.0 250 0   0   true 2 --- inspect 9.9 5.9 310 .66 0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .95 .71 66 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7 2.1 250 0   0   true 2 --- inspect 11   6.5 320 .66 0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .53 66 9.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4 1.9 250 0   0   true 2 --- inspect 19   11   470 .62 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c unknown 0 wit inspect .81 .55 66 9.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 1.9 250 0   0   true 2 --- inspect 25   15   680 .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .53 67 9.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 32   20   720 .62 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c unknown 0 wit inspect .81 .54 67 8.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.1 250 0   0   true 2 --- inspect 47   30   610 .66 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c unknown 0 wit inspect .84 .58 66 8.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 13   7.3 440 .66 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c unknown 0 wit inspect .80 .55 65 8.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 20   12   610 .62 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c unknown 0 wit inspect .79 .53 65 8.0 26    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4 1.9 250 0   0   true 2 --- inspect 26   16   520 .62 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c unknown 0 wit inspect .78 .53 66 9.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6 2.0 250 0   0   true 2 --- inspect 35   22   690 .62 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c unknown 0 wit inspect .81 .54 66 9.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5 2.0 250 0   0   true 2 --- inspect 53   35   900 .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c unknown 0 wit inspect .80 .53 69 8.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1 2.3 250 0   0   true 2 --- inspect 14   8.3 380 .66 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.1  .82 67 14   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8 2.1 250 0   0   true 2 --- inspect 13   7.4 340 .66 0  
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 96 36 4200 3900 250000 55000 2900 .0041 44 -1 520   330   34000 0   0   44 -982 690 500 16000 31   0   44 35 130 79 9300 0   0   44 36 21 22 820 1.7 .033 52 6 190 110   13000 0   0   52 82 12000 11000 73000 33 0  
    correct results 36 36 57 56 3200 840 1000 .0041 31 31 200   110   10000 0   0   10 10 170 100 4600 6.3 0   35 35 120 72 8600 0   0   36 36 21 21 730 1.7 .025 3 6 11 6.3 750 0   0   41 82 1400 920 29000 26 0  
        correct true 0 0 0 0 0 3 6 11 6.3 750 0   0   41 82 1400 920 29000 26 0  
        correct false 36 36 57 56 3200 840 1000 .0041 31 31 200   110   10000 0   0   10 10 170 100 4600 6.3 0   35 35 120 72 8600 0   0   36 36 21 21 730 1.7 .025 0 0
    incorrect results 0 1 -32 3.8 2.2 250 0   0   31 -992 240 140 9600 20   0   0 0 0 0
        incorrect true 0 1 -32 3.8 2.2 250 0   0   31 -992 240 140 9600 20   0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 36 -1 -982 35 36 6 82
Run set depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-Recursive