Tool CBMC Path 5.10 () 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-04 22:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 07:24:45 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cbmc-path.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 180     180     15000   2600    42      0      error (invalid witness file) 0 --- inspect .68 .43 40 0   0   error (2) 0 --- inspect .026 .027 5.5 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0      0     error (invalid witness file) 0 --- inspect .0057 .0069 .52 0     0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .071 .062 9.7 .77 .016  0      false(unreach-call) 1 wit inspect 6.1  3.4  270 0   0   false(unreach-call) 1 --- inspect 7.8   4.4   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.2  250 0      4.9   false(unreach-call) 1 --- inspect .61   .61   20    .049 0      - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .080 .071 8.6 .57 .041  0      true -32 wit inspect 3.9  2.2  250 0   0   true -32 --- inspect 6.8   4.3   310   .62 0   unknown 0 --- inspect 3.5  2.0  250 0      0     false(unreach-call) 1 --- 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 .070 .060 9.4 .44 .0082 0      false(unreach-call) 1 wit inspect 4.7  2.6  250 0   0   false(unreach-call) 1 --- inspect 7.7   4.4   300   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0      .40  false(unreach-call) 1 --- inspect .61   .61   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 160     160     15000   2200    120      .0041 error (invalid witness file) 0 --- inspect .78 .46 42 0   0   error (2) 0 --- inspect .028 .030 5.8 0    0   error (invalid witness file) 0 --- inspect .99 .65 49 0      0     error (invalid witness file) 0 --- inspect .0058 .0071 .52 0     0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 180     180     15000   2000    210      0      error (invalid witness file) 0 --- inspect .66 .41 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0      0     error (invalid witness file) 0 --- inspect .0017 .0022 .52 0     0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .074 .064 9.0 .36 .0082 0      false(unreach-call) 1 wit inspect 4.2  2.3  250 0   0   false(unreach-call) 1 --- inspect 7.5   4.5   310   .66 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/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 170     170     15000   1900    5.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .55 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 190     190     15000   2400    150      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .022 .023 5.5 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 190     190     15000   2400    150      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 780     780     15000   9000    790      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (134) 0 --- inspect .050 .049 6.6 .40 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     290   11000    260      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 180     180     15000   2300    200      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c witness invalid (true) 0 wit inspect .10  .098 6.4 .97 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.8   3.6   260   .61 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 180     180     15000   2100    200      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 270     270     15000   3200    180      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 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 320     320     15000   4100    420      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 --- inspect 300     290     15000   3900    250      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     15000   12000    1000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .034 .035 5.5 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 870     880     6800   11000    1100      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 180     180     15000   2200    280      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .052 .054 5.5 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .53  .53  11   6.6  .34   0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 7.4   4.3   310   .62 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .85  .84  11   12    1.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 13     7.7   500   .62 0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .093 .077 8.8 .35 .0082 0      true -32 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 6.9   3.9   300   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0      0     false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .076 .066 10   .47 .0082 0      true -32 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 10     6.0   310   .66 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0      4.6   false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .22  .21  12   1.4  .066  0      timeout 0 --- inspect 92    66    2500 0   0   timeout 0 --- inspect 98     67     5900   1.6  0   timeout 0 --- inspect 92    61    3300 0      0     false(unreach-call) 1 --- inspect .62   .63   22    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .96  .95  82   10    .52   0      exception 0 --- inspect 13    6.7  580 0   0   timeout 0 --- inspect 91     53     7000   1.7  0   timeout 0 --- inspect 12    130    610 .016  0     false(unreach-call) 1 --- inspect 1.1    1.1    43    .049 .090  - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 11     11     860   120    7.9    0      exception 0 --- inspect 76    39    3300 0   0   out of memory 0 --- inspect 86     48     7000   .63 0   timeout 0 --- inspect 59    130    3200 .0041 0     false(unreach-call) 1 --- inspect 7.0    7.0    300    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 120     120     9600   1400    71      0      timeout 0 --- inspect 98    57    4600 0   0   timeout 0 --- inspect 98     55     7000   .72 0   timeout 0 --- inspect 98    57    4900 .59   0     false(unreach-call) 1 --- inspect 72      72      3200    .049 .0041 - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .16  .14  12   1.6  .057  0      timeout 0 --- inspect 92    61    2600 0   0   timeout 0 --- inspect 98     73     5300   .63 0   timeout 0 --- inspect 97    65    3500 .020  0     false(unreach-call) 1 --- inspect .63   .63   23    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .96  .95  84   12    .53   0      exception 0 --- inspect 19    9.7  560 0   0   timeout 0 --- inspect 97     54     5800   .65 0   timeout 0 --- inspect 9.9  130    530 .033  0     false(unreach-call) 1 --- inspect 1.2    1.2    45    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 11     11     880   140    8.2    0      exception 0 --- inspect 83    43    4100 0   0   out of memory 0 --- inspect 78     43     7000   .64 0   timeout 0 --- inspect 95    130    3700 .025  0     false(unreach-call) 1 --- inspect 7.9    7.9    320    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 120     120     9800   1400    74      0      timeout 0 --- inspect 98    58    4800 0   0   out of memory 0 --- inspect 82     47     7000   .62 0   timeout 0 --- inspect 98    57    4800 .016  0     false(unreach-call) 1 --- inspect 81      81      3400    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 .071 8.9 .45 .0082 0      true -32 wit inspect 4.3  2.4  250 0   0   false(unreach-call) 1 --- inspect 10     5.9   310   .66 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0      0     false(unreach-call) 1 --- inspect .57   .58   21    .049 .38   - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .069 .060 9.4 .50 .0082 0      true -32 wit inspect 9.6  5.1  360 0   0   false(unreach-call) 1 --- inspect 23     13     510   .66 0   false(unreach-call) 1 --- inspect 4.8  2.7  260 0      1.4   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .065 .056 8.8 1.0  .0082 0      true -32 wit inspect 15    7.7  470 0   0   false(unreach-call) 1 --- inspect 26     14     590   .66 0   false(unreach-call) 1 --- inspect 7.3  4.0  330 0      0     false(unreach-call) 1 --- inspect .62   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .074 .066 9.3 .59 .0082 0      true -32 wit inspect 30    16    1000 0   0   false(unreach-call) 1 --- inspect 37     21     820   .62 0   false(unreach-call) 1 --- inspect 12    6.3  460 0      .012 false(unreach-call) 1 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  .094 9.5 1.2  .029  0      timeout 0 --- inspect 91    66    2700 0   0   timeout 0 --- inspect 96     59     3600   .64 0   false(unreach-call) 1 --- inspect 83    55    2900 0      0     false(unreach-call) 1 --- inspect .59   .59   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .12  9.3 .46 .016  0      true -32 wit inspect 12    6.5  470 0   0   false(unreach-call) 1 --- inspect 24     13     550   .62 0   false(unreach-call) 1 --- inspect 6.7  3.7  290 0      4.6   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  .13  9.3 .66 .025  0      true -32 wit inspect 72    49    2300 0   0   true -32 --- inspect 41     25     1500   .62 0   false(unreach-call) 1 --- inspect 25    14    1200 0      0     false(unreach-call) 1 --- inspect .71   .72   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 .073 .062 9.4 .40 .0082 0      false(unreach-call) 1 wit inspect 5.4  2.9  260 0   0   false(unreach-call) 1 --- inspect 9.7   5.4   310   .66 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0      4.6   false(unreach-call) 1 --- inspect .58   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .068 8.9 .46 .0082 0      true -32 wit inspect 5.6  3.1  260 0   0   false(unreach-call) 1 --- inspect 9.1   5.2   310   .62 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0      0     false(unreach-call) 1 --- inspect .60   .60   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 .070 .060 9.3 .44 .0082 0      false(unreach-call) 1 wit inspect 5.0  2.7  270 0   0   false(unreach-call) 1 --- inspect 9.1   5.5   320   .66 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-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  .11  8.9 .62 .020  0      true -32 wit inspect 7.3  4.0  270 0   0   true -32 --- inspect 8.0   4.8   300   .66 0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0      4.6   false(unreach-call) 1 --- inspect .61   .60   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .11  9.1 .79 .025  0      true -32 wit inspect 8.3  4.5  280 0   0   true -32 --- inspect 7.3   4.0   310   .62 0   false(unreach-call) 1 --- inspect 5.7  3.2  260 0      4.6   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 .13  .12  9.1 1.3  .029  0      true -32 wit inspect 7.8  4.1  340 0   0   true -32 --- inspect 7.4   4.1   290   .62 0   false(unreach-call) 1 --- inspect 4.9  2.8  260 0      0     false(unreach-call) 1 --- inspect .58   .58   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  .14  9.1 1.3  .037  0      true -32 wit inspect 9.6  5.1  430 0   0   true -32 --- inspect 7.1   4.0   300   .66 0   false(unreach-call) 1 --- inspect 5.3  3.0  270 0      .012 false(unreach-call) 1 --- inspect .60   .60   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .075 .066 9.7 .60 .012  0      true -32 wit inspect 5.9  3.3  260 0   0   false(unreach-call) 1 --- inspect 8.7   5.3   310   .66 0   false(unreach-call) 1 --- inspect 4.7  2.7  250 0      4.6   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 820     820     760   11000    .42   0      exception 0 --- inspect 10    5.5  380 0   0   true -32 --- inspect 18     9.8   1000   .62 0   timeout 0 --- inspect 8.7  130    390 .012  0     false(unreach-call) 1 --- inspect .87   .87   32    .049 0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 1.7   1.7   19   24    .14   0      timeout 0 --- inspect 92    69    2100 0   0   true -32 --- inspect 8.8   4.8   340   .66 0   false(unreach-call) 1 --- inspect 14    7.9  500 0      .012 false(unreach-call) 1 --- inspect .64   .65   21    .049 .0041 - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .21  .19  8.8 .83 .025  0      false(unreach-call) 1 wit inspect 10    5.4  430 0   0   true -32 --- inspect 8.0   4.7   300   .66 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0      1.4   false(unreach-call) 1 --- inspect .61   .60   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   48   93    .21   0      timeout 0 --- inspect 92    71    2100 0   0   true -32 --- inspect 8.9   4.8   450   .62 0   false(unreach-call) 1 --- inspect 38    27    1300 0      0     false(unreach-call) 1 --- inspect .62   .62   23    .049 0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .25  .24  9.1 2.9  .053  0      false(unreach-call) 1 wit inspect 27    14    870 0   0   true -32 --- inspect 7.0   3.9   290   .62 0   false(unreach-call) 1 --- inspect 5.2  3.0  270 0      .25  false(unreach-call) 1 --- inspect .59   .59   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .087 .075 9.2 .65 .016  0      false(unreach-call) 1 wit inspect 5.5  3.0  270 0   0   false(unreach-call) 1 --- inspect 7.3   4.5   300   .62 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0      0     false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  .090 9.4 .77 .020  0      true -32 wit inspect 6.0  3.2  270 0   0   true -32 --- inspect 6.5   4.2   300   .66 0   false(unreach-call) 1 --- inspect 4.2  2.5  250 0      4.8   false(unreach-call) 1 --- inspect .61   .62   20    .045 .016  - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .13  9.0 .94 .029  0      true -32 wit inspect 6.6  3.6  290 0   0   true -32 --- inspect 7.1   4.0   300   .62 0   false(unreach-call) 1 --- inspect 4.3  2.5  260 0      8.8   false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .13  9.0 1.3  .037  0      true -32 wit inspect 9.5  5.0  350 0   0   true -32 --- inspect 8.6   4.7   300   .66 0   false(unreach-call) 1 --- inspect 4.8  2.7  260 0      0     false(unreach-call) 1 --- inspect .57   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17  .16  9.7 1.8  .041  0      true -32 wit inspect 12    6.4  430 0   0   true -32 --- inspect 7.6   4.2   300   .66 0   false(unreach-call) 1 --- inspect 5.5  3.0  270 0      0     false(unreach-call) 1 --- inspect .59   .59   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .076 .065 9.0 .36 .0082 0      false(unreach-call) 1 wit inspect 4.5  2.5  260 0   0   false(unreach-call) 1 --- inspect 8.9   5.0   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0      0     false(unreach-call) 1 --- inspect .57   .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 .068 .060 9.1 .48 .0082 0      false(unreach-call) 1 wit inspect 4.3  2.3  250 0   0   false(unreach-call) 1 --- inspect 6.8   4.3   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0      .42  false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .047 .046 6.6 .24 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .49 43 0   0   error (invalid witness file) 0 --- inspect 6.1   3.2   270   .65 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .042 .042 6.8 .34 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .50 44 0   0   error (invalid witness file) 0 --- inspect 7.2   4.2   260   .65 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .15  .15  7.1 1.1  .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .49 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.5   270   .61 0  
recursive-simple/fibo_15_true-unreach-call.c witness invalid (true) 0 wit inspect .70  .69  26   8.2  .094  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .86 .52 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   260   .61 0  
recursive-simple/fibo_20_true-unreach-call.c witness invalid (true) 0 wit inspect 7.7   7.7   250   98    1.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 43 0   0   error (invalid witness file) 0 --- inspect 6.4   3.8   280   .61 0  
recursive-simple/fibo_25_true-unreach-call.c witness invalid (true) 0 wit inspect 89     89     2700   980    .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .50 43 0   0   error (invalid witness file) 0 --- inspect 6.0   3.6   260   .65 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c witness invalid (true) 0 wit inspect .11  .10  6.8 1.5  .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (invalid witness file) 0 --- inspect 5.3   3.2   260   .61 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c witness invalid (true) 0 wit inspect .70  .69  26   8.4  .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 43 0   0   error (invalid witness file) 0 --- inspect 4.7   3.0   250   .61 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c witness invalid (true) 0 wit inspect 7.5   7.5   240   89    1.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   270   .65 0  
recursive-simple/fibo_2calls_25_true-unreach-call.c witness invalid (true) 0 wit inspect 88     88     2600   920    .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 44 0   0   error (invalid witness file) 0 --- inspect 6.9   4.0   260   .65 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .084 .079 6.2 .18 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .87 .54 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   260   .61 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .046 .043 6.5 .43 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 43 0   0   error (invalid witness file) 0 --- inspect 6.4   3.8   260   .65 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .051 .050 6.2 .41 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .51 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.3   260   .61 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .051 .050 6.3 .26 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.0   3.2   270   .61 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .085 .084 6.9 .61 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   260   .61 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .11  .11  6.1 .31 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 42 0   0   error (invalid witness file) 0 --- inspect 6.1   3.2   270   .61 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .071 .070 6.6 .55 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .51 42 0   0   error (invalid witness file) 0 --- inspect 6.2   3.4   260   .43 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     530   12000    .19   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 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 error (42) 0 --- inspect 880     880     540   13000    .19   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .42 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     550   11000    .19   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .098 .093 6.5 .23 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   260   .65 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     530   10000    .23   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     530   11000    .23   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     540   12000    .23   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .070 .068 6.5 .56 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.2   260   .61 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .087 .083 6.8 .74 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.6   260   .26 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .17  .16  6.3 .73 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 42 0   0   error (invalid witness file) 0 --- inspect 5.5   2.9   270   .61 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .12  .12  7.6 1.1  .029  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .51 44 0   0   error (invalid witness file) 0 --- inspect 5.3   3.2   270   .61 3.4
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .055 .053 6.5 .48 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .51 42 0   0   error (invalid witness file) 0 --- inspect 5.3   3.3   270   .61 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .075 .073 6.4 .78 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 42 0   0   error (invalid witness file) 0 --- inspect 5.4   3.0   270   .61 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .11  .10  7.1 .78 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.8   3.5   270   .61 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .12  .12  6.3 1.4  .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (invalid witness file) 0 --- inspect 5.1   2.8   270   .65 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .17  .16  6.8 1.3  .029  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 42 0   0   error (invalid witness file) 0 --- inspect 6.3   3.4   260   .65 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c witness invalid (true) 0 wit inspect .059 .057 6.2 .23 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 43 0   0   error (invalid witness file) 0 --- inspect 6.0   3.6   260   .61 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     100   12000    33      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .027 .028 5.7 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 45 13000   13000   250000 170000 5600   .012 44 -598 1200 730 43000 0   0   44 -463 1200 720 69000 28   0   44 31 860 1100 39000 .72 50 44 41 190 190 8000 2.0 .50 52 0 44 26 2600 0   0   52 4 190 110 8600 19   3.4
    correct results 43 45 1100   1100   22000 14000 170   0     10 10 77 42 3400 0   0   17 17 220 130 6500 11   0   31 31 290 180 13000 0    50 41 41 190 190 8000 2.0 .50 0 2 4 20 12 800 1.2 0  
        correct true 2 4 1.4 1.4 21 19 2.0 0     0 0 0 0 0 2 4 20 12 800 1.2 0  
        correct false 41 41 1100   1100   22000 14000 160   0     10 10 77 42 3400 0   0   17 17 220 130 6500 11   0   31 31 290 180 13000 0    50 41 41 190 190 8000 2.0 .50 0 0
    incorrect results 0 19 -608 230 140 8800 0   0   15 -480 160 92 6600 9.6 0   0 0 0 0
        incorrect true 0 19 -608 230 140 8800 0   0   15 -480 160 92 6600 9.6 0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 45 -598 -463 31 41 0 4
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Recursive