Tool Pinaka 0.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*
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-06 20:14:43 CET 2018-12-07 17:00:25 CET 2018-12-07 18:15:01 CET 2018-12-07 18:51:03 CET 2018-12-12 20:55:30 CET 2018-12-07 16:17:05 CET 2018-12-07 17:47:50 CET
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options --graphml-witness witness.graphml -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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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 false(unreach-call) 1 wit inspect .37 .37 58 3.4 .0041 0     false(unreach-call) 1 wit inspect 20    10    670 0   0    false(unreach-call) 1 --- inspect 8.3   5.0   320   .62 0   false(unreach-call) 1 --- inspect 4.0 2.3  250 0      0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .37 .37 59 3.6 .0041 .057 false(unreach-call) 1 wit inspect 4.7  2.6  270 0   0    false(unreach-call) 1 --- inspect 9.6   5.4   310   .66 0   false(unreach-call) 1 --- inspect 4.9 2.8  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) 0 wit inspect .37 .38 59 2.8 .0041 0     true -32 wit inspect 3.8  2.1  250 0   0    true -32 --- inspect 9.0   5.3   310   .66 0   unknown 0 --- inspect 3.6 2.1  250 0      0   true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .35 .35 59 3.2 .0041 0     false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0    false(unreach-call) 1 --- inspect 8.8   5.2   300   .62 0   false(unreach-call) 1 --- inspect 4.0 2.4  250 0      0   false(unreach-call) 1 --- inspect .58   .59   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .48 .48 64 4.6 .0041 0     timeout 0 --- inspect 91    70    2200 0   .21 false(unreach-call) 1 --- inspect 27     15     660   .62 0   false(unreach-call) 1 --- inspect 7.9 4.3  370 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 4.6  4.6  1300 52   .0041 0     timeout 0 --- inspect 91    67    2600 0   0    timeout 0 --- inspect 98     72     3900   .66 0   timeout 0 --- inspect 94   64    2900 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .36 .36 59 3.9 .0041 0     false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0    false(unreach-call) 1 --- inspect 8.2   4.9   300   .66 0   false(unreach-call) 1 --- inspect 4.2 2.5  250 0      0   false(unreach-call) 1 --- inspect .58   .60   20    .049 .0041 - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 54    53    15000 670   .061  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 53    53    15000 680   .016  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/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 54    53    15000 750   .061  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 71    71    15000 1100   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 47    46    15000 610   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 89    88    15000 1400   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 46    45    15000 590   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .44 .44 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 42     25     1500   .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 46    45    15000 640   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 43    43    15000 700   .049  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 41    40    15000 530   .029  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 --- inspect 45    44    15000 530   .053  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 180    180    15000 2300   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 230    230    15000 3300   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    900    4400 6000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .56 .57 61 6.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 7.2   4.5   320   .62 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .58 .58 67 6.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 12     7.8   500   .66 0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 .36 59 3.3 .0041 0     true -32 wit inspect 3.5  2.0  250 0   0    false(unreach-call) 1 --- inspect 6.6   4.2   300   .66 0   false(unreach-call) 1 --- inspect 4.3 2.5  250 0      0   false(unreach-call) 1 --- inspect .60   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 .36 58 3.3 .0041 0     true -32 wit inspect 3.5  1.9  250 0   0    false(unreach-call) 1 --- inspect 12     6.5   320   .66 0   false(unreach-call) 1 --- inspect 3.7 2.2  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .52 .52 58 5.8 .0041 0     timeout 0 --- inspect 91    68    2600 0   0    timeout 0 --- inspect 96     59     5700   .63 0   timeout 0 --- inspect 92   63    3100 0      0   false(unreach-call) 1 --- inspect .62   .62   23    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 1.9  1.9  68 22   .0041 0     exception 0 --- inspect 9.4  4.9  310 0   0    timeout 0 --- inspect 97     55     5700   .68 0   timeout 0 --- inspect 8.7 130    270 1.4    0   false(unreach-call) 1 --- inspect .86   .86   45    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 18    18    630 230   .0041 0     exception 0 --- inspect 17    9.1  850 0   0    timeout 0 --- inspect 95     51     7000   .63 0   timeout 0 --- inspect 17   130    840 .0041 0   false(unreach-call) 1 --- inspect 4.1    4.1    320    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 210    210    6900 2300   .0041 0     exception 0 --- inspect 86    53    4800 0   0    timeout 0 --- inspect 92     53     7000   .63 0   timeout 0 --- inspect 82   130    4800 .0041 0   false(unreach-call) 1 --- inspect 39      39      3400    .049 .0041 - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .51 .51 59 5.3 .0041 0     timeout 0 --- inspect 98    69    2900 0   0    timeout 0 --- inspect 98     58     5300   .63 0   timeout 0 --- inspect 96   66    3100 .049  0   false(unreach-call) 1 --- inspect .60   .60   23    .049 .0041 - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 2.2  2.2  68 27   .0041 0     exception 0 --- inspect 10    5.2  300 0   0    timeout 0 --- inspect 96     60     7000   .73 0   timeout 0 --- inspect 9.6 130    280 .52   0   false(unreach-call) 1 --- inspect .88   .88   49    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 21    21    680 260   .0041 .057 exception 0 --- inspect 17    9.4  940 0   0    out of memory 0 --- inspect 88     50     7000   .63 0   timeout 0 --- inspect 14   130    940 .0041 0   false(unreach-call) 1 --- inspect 4.6    4.6    370    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 240    240    7400 3100   .0041 0     timeout 0 --- inspect 97    59    5100 0   0    timeout 0 --- inspect 98     55     5900   .65 0   timeout 0 --- inspect 98   60    5100 .074  0   false(unreach-call) 1 --- inspect 45      45      3900    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 .35 59 4.0 .0041 0     false(unreach-call) 1 wit inspect 3.9  2.2  250 0   0    false(unreach-call) 1 --- inspect 7.8   4.4   310   .66 0   false(unreach-call) 1 --- inspect 5.0 2.9  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .43 .43 59 2.9 .0041 0     false(unreach-call) 1 wit inspect 10    5.4  430 0   0    false(unreach-call) 1 --- inspect 8.6   4.8   320   .66 0   false(unreach-call) 1 --- inspect 5.6 3.1  260 0      0   false(unreach-call) 1 --- inspect .61   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .39 .39 59 3.4 .0041 0     false(unreach-call) 1 wit inspect 19    9.6  720 0   0    false(unreach-call) 1 --- inspect 24     13     730   .62 0   false(unreach-call) 1 --- inspect 10   5.4  410 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 .38 59 4.7 .0041 0     false(unreach-call) 1 wit inspect 42    25    2000 0   0    timeout 0 --- inspect 98     61     5100   .66 0   false(unreach-call) 1 --- inspect 15   8.3  700 0      0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .42 59 4.6 .0041 0     timeout 0 --- inspect 94    67    3000 0   0    timeout 0 --- inspect 97     68     4000   .66 0   timeout 0 --- inspect 92   63    3400 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 .38 59 2.9 .0041 0     false(unreach-call) 1 wit inspect 16    8.4  530 0   0    false(unreach-call) 1 --- inspect 24     13     670   .66 0   false(unreach-call) 1 --- inspect 7.7 4.2  370 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .42 59 3.7 .0041 0     timeout 0 --- inspect 92    63    2400 0   0    false(unreach-call) 1 --- inspect 44     29     1700   .66 0   false(unreach-call) 1 --- inspect 27   16    1200 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .049 0      - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .37 .37 59 3.5 .0041 0     false(unreach-call) 1 wit inspect 4.8  2.6  270 0   0    false(unreach-call) 1 --- inspect 7.7   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.7 2.1  250 0      0   false(unreach-call) 1 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 .38 59 3.3 .0041 0     false(unreach-call) 1 wit inspect 5.2  2.9  270 0   0    false(unreach-call) 1 --- inspect 8.4   5.0   310   .66 0   false(unreach-call) 1 --- inspect 4.1 2.4  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .38 .38 58 3.2 .0041 0     false(unreach-call) 1 wit inspect 5.9  3.2  270 0   0    false(unreach-call) 1 --- inspect 7.8   4.4   310   .66 0   false(unreach-call) 1 --- inspect 3.6 2.1  250 0      0   false(unreach-call) 1 --- inspect .60   .61   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 .35 59 4.3 .0041 0     false(unreach-call) 1 wit inspect 6.6  3.5  290 0   0    true -32 --- inspect 7.0   3.9   300   .62 0   false(unreach-call) 1 --- inspect 4.9 2.8  250 0      0   false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 .38 59 3.1 .0041 .057 false(unreach-call) 1 wit inspect 9.1  4.8  440 0   0    true -32 --- inspect 8.5   4.7   300   .66 0   false(unreach-call) 1 --- inspect 5.5 3.1  250 0      0   false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 .38 59 3.0 .0041 0     false(unreach-call) 1 wit inspect 12    6.4  480 0   0    true -32 --- inspect 8.2   4.9   300   .62 0   false(unreach-call) 1 --- inspect 4.5 2.5  260 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .40 .40 59 3.7 .0041 0     false(unreach-call) 1 wit inspect 17    8.5  640 0   0    true -32 --- inspect 8.8   5.1   300   .66 0   false(unreach-call) 1 --- inspect 5.3 2.9  260 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .37 58 3.2 .0041 0     false(unreach-call) 1 wit inspect 5.2  2.8  270 0   0    false(unreach-call) 1 --- inspect 8.6   5.2   300   .66 0   false(unreach-call) 1 --- inspect 3.9 2.3  250 0      0   false(unreach-call) 1 --- inspect .57   .58   20    .045 .012  - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2300   .0082 0     error (invalid witness file) 0 --- inspect .60 .36 43 0   0    error (2) 0 --- inspect .025 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0 .65 47 0      0   error (invalid witness file) 0 --- inspect .0047 .0059 .52 0     0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.2  2.2  190 26   .0041 .057 timeout 0 --- inspect 92    74    2100 0   0    true -32 --- inspect 8.5   4.6   340   .66 0   false(unreach-call) 1 --- inspect 14   7.2  460 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .40 .40 59 4.1 .0041 .057 false(unreach-call) 1 wit inspect 7.5  4.0  380 0   0    true -32 --- inspect 7.2   4.0   300   .66 0   false(unreach-call) 1 --- inspect 5.4 3.0  250 0      0   false(unreach-call) 1 --- inspect .62   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.6  7.6  720 87   .0041 0     timeout 0 --- inspect 92    72    2300 0   0    true -32 --- inspect 12     6.7   460   .66 0   false(unreach-call) 1 --- inspect 26   17    980 0      0   false(unreach-call) 1 --- inspect .59   .59   22    .049 0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .45 .45 60 4.3 .0041 0     false(unreach-call) 1 wit inspect 20    10    640 0   0    true -32 --- inspect 7.4   4.2   300   .62 0   false(unreach-call) 1 --- inspect 5.1 2.9  260 0      0   false(unreach-call) 1 --- inspect .61   .61   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .37 .38 59 3.3 .0041 0     false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0    false(unreach-call) 1 --- inspect 7.0   4.1   300   .62 0   false(unreach-call) 1 --- inspect 3.7 2.2  250 0      0   false(unreach-call) 1 --- inspect .57   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .38 59 3.7 .0041 0     false(unreach-call) 1 wit inspect 7.5  4.0  300 0   0    true -32 --- inspect 8.3   5.0   310   .66 0   false(unreach-call) 1 --- inspect 5.0 2.8  250 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 .39 .39 59 3.6 .0041 0     false(unreach-call) 1 wit inspect 9.2  4.9  440 0   0    true -32 --- inspect 6.7   3.8   300   .66 0   false(unreach-call) 1 --- inspect 5.0 2.8  260 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 .37 59 3.4 .0041 0     false(unreach-call) 1 wit inspect 12    6.3  480 0   0    true -32 --- inspect 7.3   4.4   300   .62 0   false(unreach-call) 1 --- inspect 4.7 2.7  260 0      0   false(unreach-call) 1 --- inspect .56   .56   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .39 .39 59 3.6 .0041 0     false(unreach-call) 1 wit inspect 17    8.7  700 0   0    true -32 --- inspect 8.5   5.0   300   .66 0   false(unreach-call) 1 --- inspect 6.2 3.5  260 0      0   false(unreach-call) 1 --- inspect .56   .56   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 .36 59 3.2 .0041 0     false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0    false(unreach-call) 1 --- inspect 6.5   4.2   300   .66 0   false(unreach-call) 1 --- inspect 4.5 2.6  250 0      0   false(unreach-call) 1 --- inspect .59   .58   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 .40 .40 59 3.7 .0041 0     false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0    false(unreach-call) 1 --- inspect 7.3   4.2   300   .62 0   false(unreach-call) 1 --- inspect 3.6 2.1  250 0      0   false(unreach-call) 1 --- inspect .58   .59   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .36 .36 59 3.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.8  250 0   0   true 2 --- inspect 8.7   5.1   300   .66 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .35 .35 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 7.6   4.3   310   .66 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect .44 .44 59 4.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.2  1.8  250 0   0   true 2 --- inspect 49     30     2100   .62 0  
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect 1.4  1.4  60 17   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 850     780     6300   .62 0  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 11    11    220 130   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   timeout 0 --- inspect 960     910     5500   .63 0  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 130    130    2500 1600   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0   timeout 0 --- inspect 960     910     5900   .63 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .45 .45 59 5.2 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0   true 2 --- inspect 83     53     3800   .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 1.3  1.3  60 16   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   timeout 0 --- inspect 960     900     5100   .64 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 12    12    230 150   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   timeout 0 --- inspect 960     900     5500   .68 0  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 130    130    2500 1700   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   timeout 0 --- inspect 960     900     5200   1.2  0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .36 .36 59 3.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 12     6.8   390   .62 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .38 .38 59 3.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 17     10     540   .66 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .36 .37 59 3.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 27     16     500   .66 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .37 .37 59 3.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 31     19     750   .62 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .40 .40 59 4.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.2  250 0   0   true 2 --- inspect 56     35     1100   .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .36 .36 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 17     10     540   .66 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .38 .38 59 3.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 23     14     680   .62 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    200    15000 2400   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    200    15000 2600   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 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 out of memory 0 --- inspect 200    200    15000 2600   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 42 0   0   error (2) 0 --- inspect .024 .025 5.5 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .37 .38 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  2.0  250 0   0   true 2 --- inspect 17     10     500   .62 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    200    15000 2900   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .028 .030 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 470    470    15000 6600   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 470    470    15000 5400   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .36 .36 59 3.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 19     12     520   .66 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .38 .38 58 3.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.0  250 0   0   true 2 --- inspect 24     15     630   .66 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .39 .39 58 3.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 38     23     570   .66 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .38 .38 59 3.1 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 39     25     750   .62 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .37 .37 58 3.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 12     7.0   440   .62 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .41 .41 59 3.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 21     13     570   .66 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .42 .41 59 3.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 30     19     650   .62 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .39 .39 59 3.4 .0041 .057 - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 34     23     700   .62 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .39 .39 58 4.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0   true 2 --- inspect 57     37     810   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .39 .39 59 2.9 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 11     6.8   380   .66 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 86    85    15000 1100   .025  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    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 99 4700    4700    350000 55000   .92   .34  44 -70 1300 840   45000 0   .21 44 -397 1400 840 76000 28   0   44 32 830 1100 36000 2.0 0   44 10 120    120    8800 2.1   .033 52 6 120 70   8600 0   0   52 52 6300 5700 54000 20 0  
    correct results 68 94 530    530    22000 6300   .28   .34  26 26 280 150   12000 0   0    19 19 240 140 8300 12   0   32 32 220 130 11000 0   0   42 42 120    120    8800 2.0   .033 3 6 10 5.7 750 0   0   26 52 1500 1200 26000 17 0  
        correct true 26 52 11    11    1500 110   .11   .057 0 0 0 0 3 6 10 5.7 750 0   0   26 52 1500 1200 26000 17 0  
        correct false 42 42 520    520    20000 6200   .17   .29  26 26 280 150   12000 0   0    19 19 240 140 8300 12   0   32 32 220 130 11000 0   0   42 42 120    120    8800 2.0   .033 0 0
    correct-unconfimed results 6 5 290    290    5500 3600   .025  0     0 0 0 0 0 0
        correct-unconfirmed true 5 5 290    290    5400 3600   .020  0     0 0 0 0 0 0
        correct-unconfirmed false 1 0 .37 .38 59 2.8 .0041 0     0 0 0 0 0 0
    incorrect results 0 3 -96 11 6.0 750 0   0    13 -416 110 62 4100 8.4 0   0 1 -32 .57 .57 20 .049 0     0 0
        incorrect true 0 3 -96 11 6.0 750 0   0    13 -416 110 62 4100 8.4 0   0 1 -32 .57 .57 20 .049 0     0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 99 -70 -397 32 10 6 52
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Recursive