Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 02:16:29 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 .21  .21  28 2.5  .85 0   false(unreach-call) 1 wit inspect 6.9  3.8  280 0   0      true -32 --- inspect 8.0   4.8   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .12  .12  26 1.4  .85 0   false(unreach-call) 1 wit inspect 5.5  3.1  270 0   0      true -32 --- inspect 8.6   5.4   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .087 .087 26 .91 1.0  0   true -32 wit inspect 3.6  2.0  250 0   0      true -32 --- inspect 6.9   3.9   300   .62 0   unknown 0 --- inspect 4.2  2.5  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .11  .12  26 .99 1.0  0   false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0      false(unreach-call) 1 --- inspect 7.7   4.7   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/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .11  .11  26 1.3  .85 0   false(unreach-call) 1 wit inspect 33    20    600 0   0      true -32 --- inspect 7.7   4.4   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/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.5   3.5   96 42    1.0  0   false(unreach-call) 1 wit inspect 72    57    810 0   0      true -32 --- inspect 7.6   4.8   310   .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .084 .085 26 1.1  1.0  0   false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 7.6   4.7   310   .62 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/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 610     600     15000 7400    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 560     540     15000 5900    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 620     600     15000 6800    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 42 0   0   error (2) 0 --- inspect .023 .024 5.8 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 850     810     15000 8500    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .029 .029 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 850     810     15000 8200    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .033 .035 5.5 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     1200 11000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 270     260     15000 3100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .028 .030 5.7 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .12  .11  26 1.4  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.4  250 0   0   true 2 --- inspect 38     23     1100   .66 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 260     250     15000 2600    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     14000 8600    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 540     530     15000 5300    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 --- inspect 760     740     15000 7800    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .44 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     260 9800    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .028 .029 5.8 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     190 9300    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .49 41 0   0   error (2) 0 --- inspect .031 .032 5.6 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 510     500     15000 5100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .26  .25  26 3.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 7.9   4.4   310   .66 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .39  .38  26 5.3  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.3  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 .079 .080 26 .92 .85 0   false(unreach-call) 1 wit inspect 4.7  2.6  250 0   0      true -32 --- inspect 6.5   4.1   290   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .083 .085 26 .85 1.0  0   false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0      true -32 --- inspect 7.7   4.4   310   .62 0   false(unreach-call) 1 --- inspect 3.5  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 .14  .13  26 1.5  1.0  0   false(unreach-call) 1 wit inspect 7.3  4.1  330 0   0      true -32 --- inspect 7.8   4.5   310   .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .82  .76  29 11    1.0  0   false(unreach-call) 1 wit inspect 23    14    1200 0   0      true -32 --- inspect 8.5   4.8   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 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 14     13     220 180    1.0  0   out of memory 0 --- inspect 45    35    7000 0   0      true -32 --- inspect 7.7   4.4   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 210     190     2400 2700    1.0  0   timeout 0 --- inspect 97    64    3600 0   0      true -32 --- inspect 9.4   5.1   320   .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  26 1.2  1.0  0   false(unreach-call) 1 wit inspect 7.1  4.0  330 0   0      true -32 --- inspect 9.3   5.5   310   .62 0   false(unreach-call) 1 --- inspect 3.3  1.9  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .75  .68  27 9.1  1.0  0   false(unreach-call) 1 wit inspect 23    16    1200 0   0      true -32 --- inspect 9.9   5.8   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/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 8.1   7.6   160 110    1.0  0   out of memory 0 --- inspect 44    34    7000 0   0      true -32 --- inspect 7.6   4.8   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 120     110     1700 1400    1.0  0   timeout 0 --- inspect 97    63    3900 0   0      true -32 --- inspect 9.4   5.2   310   .66 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_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .087 .088 26 .87 1.0  0   false(unreach-call) 1 wit inspect 3.8  2.2  250 0   0      true -32 --- inspect 8.1   5.1   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-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  26 .94 1.0  0   false(unreach-call) 1 wit inspect 4.6  2.6  260 0   0      true -32 --- inspect 8.2   5.0   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  26 .99 .85 0   false(unreach-call) 1 wit inspect 5.5  3.1  260 0   0      true -32 --- inspect 7.9   4.5   310   .62 0   false(unreach-call) 1 --- inspect 3.9  2.3  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 .088 .089 26 .78 .85 0   false(unreach-call) 1 wit inspect 5.0  2.8  270 0   0      true -32 --- inspect 8.2   4.9   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .61   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .11  26 1.2  1.0  0   false(unreach-call) 1 wit inspect 6.8  3.8  290 0   .016  true -32 --- inspect 8.2   4.9   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_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .083 .083 26 1.1  .85 0   false(unreach-call) 1 wit inspect 4.6  2.6  270 0   0      true -32 --- inspect 9.0   5.1   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .092 .092 26 1.1  1.0  0   false(unreach-call) 1 wit inspect 5.4  3.0  280 0   0      true -32 --- inspect 8.7   4.9   310   .62 0   false(unreach-call) 1 --- inspect 4.0  2.4  250 0   0   false(unreach-call) 1 --- inspect .57   .57   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 .089 .090 26 1.0  1.0  0   false(unreach-call) 1 wit inspect 4.9  2.7  270 0   0      false(unreach-call) 1 --- inspect 8.1   5.0   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 .082 26 .89 .85 0   false(unreach-call) 1 wit inspect 4.4  2.5  260 0   0      true -32 --- inspect 7.7   4.6   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 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 .11  .11  26 .92 1.0  0   false(unreach-call) 1 wit inspect 4.4  2.5  260 0   0      false(unreach-call) 1 --- inspect 8.8   5.5   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .090 .091 26 1.1  1.0  0   false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0      true -32 --- inspect 7.3   4.1   310   .62 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  26 .96 1.0  0   false(unreach-call) 1 wit inspect 5.2  2.9  270 0   0      true -32 --- inspect 7.9   4.3   320   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  26 1.7  1.0  0   false(unreach-call) 1 wit inspect 5.1  2.8  270 0   0      true -32 --- inspect 7.5   4.3   310   .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/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  26 1.6  .85 0   false(unreach-call) 1 wit inspect 5.4  3.0  270 0   0      true -32 --- inspect 8.0   4.8   320   .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .085 .085 26 .90 1.0  0   false(unreach-call) 1 wit inspect 5.0  2.8  260 0   0      true -32 --- inspect 7.9   4.8   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .59   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1200 11000    .86 0   error (invalid witness file) 0 --- inspect .68 .41 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 49 0   0   error (invalid witness file) 0 --- inspect .0042 .0053 .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.1   34 30    .85 0   false(unreach-call) 1 wit inspect 71    53    2100 0   0      true -32 --- inspect 9.1   5.2   320   .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .11  .11  26 1.2  1.0  0   false(unreach-call) 1 wit inspect 6.7  3.7  280 0   0      true -32 --- inspect 8.1   4.7   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/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 13     13     86 160    1.0  0   timeout 0 --- inspect 91    74    2200 0   0      true -32 --- inspect 9.2   5.3   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/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .15  .14  26 2.0  1.0  0   false(unreach-call) 1 wit inspect 9.7  5.4  420 0   0      true -32 --- inspect 9.0   5.6   310   .62 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/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .085 .085 26 .85 .85 0   false(unreach-call) 1 wit inspect 4.4  2.4  270 0   0      true -32 --- inspect 8.3   5.2   310   .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  26 1.0  .85 0   false(unreach-call) 1 wit inspect 5.1  2.8  270 0   0      true -32 --- inspect 8.0   4.5   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 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 .096 .095 26 1.2  1.0  0   false(unreach-call) 1 wit inspect 4.6  2.6  270 0   0      true -32 --- inspect 7.4   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  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 .11  .11  26 1.3  1.0  0   false(unreach-call) 1 wit inspect 5.1  2.8  270 0   .0041 true -32 --- inspect 7.8   4.7   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.0  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 .12  .12  26 1.3  .85 0   false(unreach-call) 1 wit inspect 6.2  3.4  280 0   0      true -32 --- inspect 7.5   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/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .081 .081 26 .80 .85 0   false(unreach-call) 1 wit inspect 4.4  2.5  260 0   0      true -32 --- inspect 7.6   4.7   310   .62 0   false(unreach-call) 1 --- inspect 3.4  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 .081 .083 26 1.0  1.0  0   false(unreach-call) 1 wit inspect 4.2  2.3  250 0   0      false(unreach-call) 1 --- inspect 7.3   4.6   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .076 .078 26 .86 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 8.5   4.7   320   .66 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .10  .11  26 .82 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 7.2   4.6   310   .66 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect .15  .14  26 1.8  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.5  250 0   0   true 2 --- inspect 49     32     2800   .62 0  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect .94  .88  30 13    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   timeout (true) 0 --- inspect 900     840     6300   .62 0  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 16     15     230 210    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.5  250 0   0   timeout 0 --- inspect 960     920     4900   1.7  0  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 230     220     2600 2600    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0   timeout 0 --- inspect 920     870     7000   .64 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .12  .12  26 1.4  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0   true 2 --- inspect 100     66     3200   .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect .78  .73  28 11    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 5.3  3.0  250 0   0   timeout 0 --- inspect 960     900     5500   .70 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 9.9   9.3   180 130    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   timeout 0 --- inspect 960     880     6100   1.7  0  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 140     130     1900 1800    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.6  250 0   0   timeout 0 --- inspect 960     890     5100   .63 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .079 .080 26 .89 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  250 0   0   true 2 --- inspect 14     8.4   390   .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .082 .084 26 .97 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.2  250 0   0   true 2 --- inspect 19     12     540   .66 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .085 .085 26 .88 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0   true 2 --- inspect 29     18     500   .66 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .088 .089 26 .97 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 40     24     750   .62 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .10  .10  26 1.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 48     30     1100   .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .086 .086 26 .87 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.5  250 0   0   true 2 --- inspect 20     12     470   .66 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .11  .11  26 .87 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.3  250 0   0   true 2 --- inspect 24     14     700   .62 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1200 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .50 42 0   0   error (2) 0 --- inspect .030 .031 5.6 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1200 9700    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     1200 9500    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .086 .089 26 .80 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.6  250 0   0   true 2 --- inspect 16     10     510   .62 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1200 10000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .027 .029 5.7 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     950 10000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 43 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     960 13000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 43 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 .11  .11  26 1.0  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 20     12     530   .66 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .097 .096 26 1.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 24     15     630   .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .13  .13  26 1.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 29     18     690   .66 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  26 1.3  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0   true 2 --- inspect 39     24     610   .66 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .084 .084 26 .89 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 12     6.8   430   .62 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .089 .088 26 1.0  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 23     14     580   .66 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .10  .10  26 1.2  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.4  250 0   0   true 2 --- inspect 27     17     530   .66 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .13  .13  26 1.1  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.8  2.6  250 0   0   true 2 --- inspect 39     25     760   .66 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .13  .13  26 1.6  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 53     35     670   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .083 .083 26 .80 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 5.5  3.0  250 0   0   true 2 --- inspect 12     7.3   380   .66 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     250 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0   error (2) 0 --- inspect .026 .026 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 17000   17000   190000 190000 92   0   44 5 770   530   39000 0   .020 44 -1211 350 210 13000 27   0   44 42 150 90 11000 0   0   44 43 25 25 870 2.1 .020 52 6 150 83   8600 0   0   52 50 6400 5800 54000 22 0  
    correct results 68 93 370   350   6200 4800 65   0   37 37 390   260   15000 0   .020 5 5 39 25 1500 3.1 0   42 42 150 86 10000 0   0   43 43 25 25 870 2.1 .020 3 6 12 6.9 750 0   0   25 50 720 440 19000 16 0  
        correct true 25 50 3.0 3.0 650 33 24   0   0 0 0 0 3 6 12 6.9 750 0   0   25 50 720 440 19000 16 0  
        correct false 43 43 370   350   5600 4700 41   0   37 37 390   260   15000 0   .020 5 5 39 25 1500 3.1 0   42 42 150 86 10000 0   0   43 43 25 25 870 2.1 .020 0 0
    correct-unconfimed results 6 6 400   380   4900 4800 5.6 0   0 0 0 0 0 0
        correct-unconfirmed true 6 6 400   380   4900 4800 5.6 0   0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 1 -32 3.6 2.0 250 0   0     38 -1216 310 180 12000 24   0   0 0 0 0
        incorrect true 0 1 -32 3.6 2.0 250 0   0     38 -1216 310 180 12000 24   0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 99 5 -1211 42 43 6 50
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Recursive