Tool skink 2.0 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*
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-07 12:00:55 CET 2018-12-07 18:03:00 CET 2018-12-07 19:11:22 CET 2018-12-07 19:49:22 CET 2018-12-12 21:02:00 CET 2018-12-07 17:09:07 CET 2018-12-07 18:50:30 CET
Run set skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-skink.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/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/skink.2018-12-07_1200.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/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/skink.2018-12-07_1200.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 unknown 0 --- inspect 7.6 3.5 220 69 .13   0      error (invalid witness file) 0 --- inspect .74 .45 42 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0068 .54 0     0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 7.9 2.9 350 67 .037  0      false(unreach-call) 1 wit inspect 6.0  3.3  270 0   0   true -32 --- inspect 8.0   5.0   310   .62 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0   false(unreach-call) 1 --- inspect .58   .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 7.8 2.9 320 72 .037  0      false(unreach-call) 1 wit inspect 4.3  2.4  250 0   0   true -32 --- inspect 6.3   3.6   300   .66 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 5.9 2.4 310 52 .037  0      false(unreach-call) 1 wit inspect 5.4  3.0  260 0   0   false(unreach-call) 1 --- inspect 9.2   5.3   300   .66 0   false(unreach-call) 1 --- inspect 4.3  2.6  250 0   0   false(unreach-call) 1 --- inspect .61   .63   20    .049 .0041 - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.7 3.5 220 77 .12   0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 48 0   0   error (invalid witness file) 0 --- inspect .0055 .0078 .39 0     0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.7 3.5 220 71 .12   0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0038 .0048 .52 0     0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.6 3.5 220 69 .13   0      error (invalid witness file) 0 --- inspect .78 .48 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0   error (invalid witness file) 0 --- inspect .0047 .0060 .52 0     0      - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 7.0 3.5 220 77 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 7.6 3.5 230 73 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 7.4 3.5 230 75 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 210   200   740 2500 .0041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.0  250 0   0   true 2 --- inspect 11     6.2   390   .66 0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 850   770   5100 10000 23      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .028 .030 5.7 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 400   340   1100 3200 28      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 7.2 3.5 220 83 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.2 3.5 210 67 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.2 3.5 220 71 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.5 3.5 220 69 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   3400 5000 .029  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 --- inspect 9.0 3.8 280 87 .26   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 41   26   1100 470 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 9.9   6.1   350   .66 0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 98   68   1600 1100 38      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 8.1 3.6 230 73 .14   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.7 3.5 220 72 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 7.5 3.5 220 67 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c unknown 0 --- inspect 7.6 3.5 220 74 .12   0      error (invalid witness file) 0 --- inspect .63 .40 40 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 48 0   0   error (invalid witness file) 0 --- inspect .0045 .0056 .52 0     0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c unknown 0 --- inspect 7.4 3.4 210 71 .10   0      error (invalid witness file) 0 --- inspect .71 .44 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 47 0   0   error (invalid witness file) 0 --- inspect .0064 .0088 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c unknown 0 --- inspect 7.4 3.4 220 71 .12   0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 47 0   0   error (invalid witness file) 0 --- inspect .0050 .0069 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c unknown 0 --- inspect 7.2 3.4 220 71 .11   0      error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 48 0   0   error (invalid witness file) 0 --- inspect .0015 .0020 .41 0     0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c unknown 0 --- inspect 7.3 3.5 220 71 .11   0      error (invalid witness file) 0 --- inspect .69 .44 42 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0035 .0047 .52 0     0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c unknown 0 --- inspect 7.3 3.5 220 67 .11   0      error (invalid witness file) 0 --- inspect .81 .50 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .61 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0065 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c unknown 0 --- inspect 7.5 3.5 240 82 .15   0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0070 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c unknown 0 --- inspect 7.8 3.6 240 67 .15   0      error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 47 0   0   error (invalid witness file) 0 --- inspect .0052 .0066 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c unknown 0 --- inspect 7.5 3.5 240 71 .15   0      error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0042 .0054 .39 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c unknown 0 --- inspect 7.3 3.6 240 79 .15   0      error (invalid witness file) 0 --- inspect .79 .49 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0056 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.4 2.2 300 57 .037  0      false(unreach-call) 1 wit inspect 4.7  2.6  250 0   0   true -32 --- inspect 6.7   3.8   300   .66 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect .61   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c unknown 0 --- inspect 8.0 3.6 240 84 .15   .0041 error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.4  .88 47 0   0   error (invalid witness file) 0 --- inspect .0043 .0058 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c unknown 0 --- inspect 7.9 3.6 240 77 .15   0      error (invalid witness file) 0 --- inspect .61 .39 41 0   0   error (2) 0 --- inspect .028 .029 5.8 0    0   error (invalid witness file) 0 --- inspect 1.4  .87 48 0   0   error (invalid witness file) 0 --- inspect .0036 .0047 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c unknown 0 --- inspect 8.2 3.7 250 86 .15   0      error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .79 47 0   0   error (invalid witness file) 0 --- inspect .0048 .0064 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c unknown 0 --- inspect 8.0 3.6 240 78 .15   0      error (invalid witness file) 0 --- inspect .71 .45 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 49 0   0   error (invalid witness file) 0 --- inspect .0051 .0065 .52 0     0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c unknown 0 --- inspect 6.9 3.4 220 74 .12   0      error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .57 47 0   0   error (invalid witness file) 0 --- inspect .0026 .013  .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c unknown 0 --- inspect 7.4 3.4 220 79 .12   0      error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .051 .052 5.5 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 46 0   0   error (invalid witness file) 0 --- inspect .0054 .0068 .52 0     0      - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.8 3.5 230 77 .13   0      error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0   error (invalid witness file) 0 --- inspect .0022 .0029 .54 0     0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c unknown 0 --- inspect 7.0 3.4 220 71 .12   0      error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .031 .032 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0   error (invalid witness file) 0 --- inspect .0049 .0077 .52 0     0      - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.4 3.4 220 74 .11   0      error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0056 .53 0     0      - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.9 2.1 260 44 .037  0      false(unreach-call) 1 wit inspect 5.0  2.8  260 0   0   true -32 --- inspect 6.6   3.8   290   .66 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect .59   .60   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.7 2.1 270 45 .037  0      false(unreach-call) 1 wit inspect 5.6  3.1  260 0   0   true -32 --- inspect 6.7   3.7   300   .66 0   false(unreach-call) 1 --- inspect 4.2  2.5  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.1 2.1 260 50 .037  0      false(unreach-call) 1 wit inspect 5.6  3.1  270 0   0   true -32 --- inspect 8.0   4.7   300   .66 0   false(unreach-call) 1 --- inspect 4.9  2.8  250 0   0   false(unreach-call) 1 --- inspect .60   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.0 2.2 270 45 .037  0      false(unreach-call) 1 wit inspect 5.5  3.0  270 0   0   true -32 --- inspect 8.2   5.0   290   .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 2.2 270 45 .037  0      false(unreach-call) 1 wit inspect 5.2  2.9  260 0   0   true -32 --- inspect 7.3   4.1   300   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.2 2.2 260 49 .037  0      timeout 0 --- inspect 91    74    2400 0   0   true -32 --- inspect 7.3   4.1   310   .62 0   false(unreach-call) 1 --- inspect 4.5  2.6  240 0   0   false(unreach-call) 1 --- inspect .58   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.3 2.3 280 50 .037  0      false(unreach-call) 1 wit inspect 8.6  4.6  450 0   0   true -32 --- inspect 7.9   4.5   310   .66 0   false(unreach-call) 1 --- inspect 4.4  2.6  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.0 2.2 270 43 .037  0      false(unreach-call) 1 wit inspect 5.5  3.0  260 0   0   true -32 --- inspect 9.7   5.3   310   .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .63   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.5 2.3 290 53 .037  0      false(unreach-call) 1 wit inspect 14    7.4  680 0   0   true -32 --- inspect 9.0   5.0   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.4 2.2 270 51 .037  0      false(unreach-call) 1 wit inspect 6.4  3.5  270 0   0   true -32 --- inspect 8.6   4.9   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.8 2.4 290 52 .037  0      false(unreach-call) 1 wit inspect 5.6  3.1  260 0   0   true -32 --- inspect 9.2   5.2   320   .66 0   false(unreach-call) 1 --- inspect 4.8  2.8  250 0   0   false(unreach-call) 1 --- inspect .61   .60   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.3 2.2 280 46 .037  0      false(unreach-call) 1 wit inspect 4.9  2.7  270 0   0   true -32 --- inspect 7.1   4.4   290   .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.8 2.1 270 49 .037  0      false(unreach-call) 1 wit inspect 4.5  2.5  270 0   0   true -32 --- inspect 6.3   3.6   300   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.1 2.1 270 47 .037  0      false(unreach-call) 1 wit inspect 4.6  2.5  270 0   0   true -32 --- inspect 8.5   5.0   300   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.1 2.1 270 46 .037  0      false(unreach-call) 1 wit inspect 6.3  3.5  270 0   0   true -32 --- inspect 7.9   4.3   300   .66 0   false(unreach-call) 1 --- inspect 4.4  2.6  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.1 2.1 270 46 .037  0      false(unreach-call) 1 wit inspect 5.0  2.8  260 0   0   true -32 --- inspect 7.6   4.1   300   .66 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0   false(unreach-call) 1 --- inspect .56   .56   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 4.8 2.1 270 44 .037  0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 7.7   4.3   310   .66 0   false(unreach-call) 1 --- inspect 4.7  2.7  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 4.2 1.9 230 40 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 7.7   4.3   320   .62 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.7 220 32 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 9.3   5.3   310   .66 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c unknown 0 --- inspect 7.1 3.4 220 68 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0  
recursive-simple/fibo_15_true-unreach-call.c unknown 0 --- inspect 7.2 3.5 220 79 .11   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/fibo_20_true-unreach-call.c unknown 0 --- inspect 7.3 3.5 220 68 .11   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive-simple/fibo_25_true-unreach-call.c unknown 0 --- inspect 7.2 3.5 220 68 .11   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive-simple/fibo_2calls_10_true-unreach-call.c unknown 0 --- inspect 8.0 3.6 240 78 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .028 .029 5.7 0    0  
recursive-simple/fibo_2calls_15_true-unreach-call.c unknown 0 --- inspect 8.1 3.6 250 76 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/fibo_2calls_20_true-unreach-call.c unknown 0 --- inspect 8.2 3.7 240 77 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive-simple/fibo_2calls_25_true-unreach-call.c unknown 0 --- inspect 7.8 3.5 240 81 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 3.9 1.9 240 38 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 11     7.0   390   .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c unknown 0 --- inspect 8.0 3.6 240 76 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c unknown 0 --- inspect 8.1 3.6 250 76 .15   .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c unknown 0 --- inspect 7.5 3.5 240 82 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c unknown 0 --- inspect 7.8 3.5 240 78 .15   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c unknown 0 --- inspect 7.5 3.5 220 73 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c unknown 0 --- inspect 7.1 3.5 220 74 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.7 3.5 230 78 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.5 3.6 230 80 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.9 3.5 230 77 .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c unknown 0 --- inspect 7.7 3.5 220 80 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .027 .028 5.8 0    0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.6 3.5 220 86 .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.5 3.4 220 70 .11   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect 7.0 3.4 220 69 .11   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 3.4 1.7 210 36 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 18     11     520   .66 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 3.7 1.7 210 37 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 24     15     620   .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.7 210 31 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 30     18     710   .66 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.8 210 37 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  260 0   0   true 2 --- inspect 44     28     620   .66 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.8 210 39 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 11     7.1   450   .66 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.7 220 35 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 23     14     580   .62 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 3.6 1.8 220 32 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 30     18     660   .62 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.8 220 43 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 36     23     600   .62 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 4.0 1.8 220 38 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 49     32     690   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.8 220 31 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 14     8.1   380   .66 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.9 1.8 220 39 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 10     5.8   330   .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 53 3100 2500 35000 28000 99    .012 44 20 220 150 9200 0   0   44 -606 160 94   6500 14   0   44 21 110 65 6300 0   0   44 21 12 12 440 .99 .0082 52 6 78 45   5500 0   0   52 32 340 210 8100 10 0  
    correct results 37 53 420 300 11000 4600 1.3  0     20 20 120 64 5900 0   0   2 2 17 9.7 620 1.3 0   21 21 85 49 5200 0   0   21 21 12 12 430 .99 .0082 3 6 11 5.9 750 0   0   16 32 340 210 7900 10 0  
        correct true 16 32 300 250 4800 3500 .56 0     0 0 0 0 3 6 11 5.9 750 0   0   16 32 340 210 7900 10 0  
        correct false 21 21 110 47 5900 1100 .77 0     20 20 120 64 5900 0   0   2 2 17 9.7 620 1.3 0   21 21 85 49 5200 0   0   21 21 12 12 430 .99 .0082 0 0
    incorrect results 0 0 19 -608 150 84   5700 12   0   0 0 0 0
        incorrect true 0 0 19 -608 150 84   5700 12   0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 53 20 -606 21 21 6 32
Run set skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-Recursive