Tool VeriAbs 1.3.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-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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 1 670   670   200 5700 .43 .27   -32 4.3  2.4  260 0   0      1 15     8.0   400   .66 0      0 3.8  2.2  250 0   0      1 .58   .58   20    .049  0      - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 570   570   2200 5200 .77 0      -32 4.9  2.7  260 0   .0041 -32 9.4   5.4   300   .66 0      0 3.5  2.0  250 0   0      1 .58   .58   20    .049  0      - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 8.5 3.4 270 78 .13 0      0 3.3  1.9  200 0   0      -32 6.6   3.8   300   .62 0      0 3.6  2.1  200 0   0      0 .52   .52   20    .0041 0      - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 9.2 3.7 300 77 .13 0      -32 4.3  2.4  260 0   0      1 8.6   4.8   310   .66 0      0 3.8  2.1  250 0   0      1 .61   .61   20    .049  0      - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 670   660   200 4600 .43 0      -32 5.4  2.9  260 0   0      1 19     10     610   .66 0      0 3.5  2.0  250 0   0      1 .58   .58   21    .049  0      - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 1 700   690   200 5400 .57 0      -32 5.6  3.0  270 0   0      0 97     77     3600   .67 0      0 4.4  2.4  260 0   0      1 .63   .64   21    .049  0      - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 670   660   200 4600 .41 0      -32 4.2  2.3  260 0   0      1 8.1   4.5   310   .66 0      0 3.6  2.1  250 0   0      1 .59   .59   20    .049  0      - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 900   890   700 6900 .63 .0041 - - - - 0 .59 .37 41 0   0      0 .020 .021 5.6 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 900   890   740 7100 .73 0      - - - - 0 .74 .45 42 0   0      0 .021 .022 5.6 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 900   890   710 7200 .66 0      - - - - 0 .61 .39 41 0   0      0 .021 .022 5.6 0    0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 870   860   3600 6500 1.0  0      - - - - 0 .59 .36 41 0   0      0 .022 .022 5.6 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 2 72   36   1700 660 150    0      - - - - 0 3.5  1.9  250 0   .0041 2 470     370     2100   .62 0     
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 10   4.0 200 92 .33 0      - - - - 0 .78 .47 40 0   0      0 .021 .021 5.6 0    0     
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 2 840   830   660 9800 150    0      - - - - 0 3.8  2.2  250 0   0      2 18     11     480   .66 0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 51   23   3100 540 140    0      - - - - 0 4.0  2.3  250 0   0      2 39     23     1300   .66 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 2 880   850   3600 7700 150    0      - - - - 0 4.4  2.5  250 0   0      2 33     20     1100   .66 0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 840   830   450 5800 160    0      - - - - 0 4.1  2.3  250 0   0      2 9.3   5.3   320   .66 0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900   890   3600 10000 .59 0      - - - - 0 .60 .37 40 0   0      0 .020 .020 5.6 0    0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900   890   3800 9000 2.2  0      - - - - 0 .60 .37 42 0   0      0 .020 .021 5.6 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900   890   2600 8100 .41 0      - - - - 0 .80 .47 41 0   0      0 .025 .026 5.5 0    0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900   890   3400 9000 .47 0      - - - - 0 .62 .39 40 0   0      0 .021 .021 5.6 0    0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 1 590   550   3800 3800 150    0      - - - - 0 4.6  2.5  250 0   0      0 960     890     6300   .65 0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 9.5 3.5 200 79 .32 0      - - - - 0 .59 .37 40 0   0      0 .023 .024 5.6 0    0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 9.3 3.5 200 85 .32 0      - - - - 0 .59 .35 41 0   0      0 .020 .020 5.6 0    0     
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 8.7 3.4 270 72 .13 0      -32 4.4  2.5  250 0   0      1 8.1   4.8   300   .66 0      0 3.4  2.0  240 0   0      1 .57   .57   20    .045  0      - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 8.3 3.3 270 68 .12 0      -32 3.6  2.0  250 0   0      1 8.4   4.8   310   .62 0      0 3.9  2.2  250 0   0      1 .58   .57   20    .045  0      - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 1 9.0 3.6 300 70 .23 .27   -32 4.8  2.6  270 0   0      0 97     64     5400   1.5  0      0 4.5  2.5  270 0   0      1 .61   .61   22    .049  0      - -
recursive-simple/fibo_15_false-unreach-call.c 1 11   5.7 270 99 1.8  .63   -32 11    5.5  600 0   0      0 96     52     5700   1.4  0      0 8.4  4.5  570 0   0      1 1.1    1.1    42    .049  0      - -
recursive-simple/fibo_20_false-unreach-call.c 1 50   45   820 460 22    0      -32 60    31    3300 0   0      0 93     50     7000   .64 0      0 61    32    3200 0   0      1 6.7    6.7    270    .049  0      - -
recursive-simple/fibo_25_false-unreach-call.c 1 310   310   7300 2200 .23 0      0 97    63    3600 0   .14   -32 8.0   4.5   300   .66 0      1 3.6  2.1  250 0   0      1 .60   .59   20    .049  0      - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 8.7 3.6 260 81 .23 0      -32 5.3  2.8  300 0   0      0 97     64     5100   1.5  0      0 5.0  2.7  260 0   0      1 .62   .62   22    .049  .0041 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 11   5.7 290 110 2.0  0      -32 8.6  4.6  640 0   0      0 91     52     7000   .63 0      0 16    8.4  660 0   0      1 1.2    1.2    43    .049  0      - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 1 52   47   830 580 28    .0041 -32 70    36    4100 0   0      0 98     52     6200   .69 0      0 69    36    3500 0   .0041 1 7.5    7.5    290    .049  0      - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 1 370   370   7200 3300 .11 0      0 97    65    3700 0   0      -32 7.9   4.4   310   .66 .0041 1 3.6  2.0  250 0   0      1 .58   .58   20    .049  .0041 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 8.9 3.4 290 83 .12 .0041 -32 3.7  2.0  250 0   0      1 9.7   5.3   310   .66 0      0 3.9  2.2  250 0   .0041 1 .57   .57   20    .049  0      - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 9.0 3.5 290 76 .13 0      -32 4.5  2.5  260 0   0      1 19     11     530   .66 0      0 3.5  2.0  250 0   0      1 .58   .58   20    .049  0      - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 8.8 3.3 290 74 .13 0      -32 4.1  2.3  260 0   0      1 23     13     640   .62 0      0 3.5  2.0  250 0   0      1 .57   .57   20    .049  0      - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 8.8 3.5 260 79 .14 .0041 -32 4.8  2.6  270 0   0      1 33     18     850   .62 0      0 3.7  2.1  250 0   0      1 .60   .61   21    .049  0      - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 1 8.8 3.4 270 79 .16 0      -32 4.5  2.5  270 0   .0041 0 97     59     3300   .63 0      0 4.1  2.3  270 0   0      1 .59   .58   21    .049  0      - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 9.0 3.5 290 76 .13 0      -32 4.9  2.7  260 0   .029  1 21     12     520   .66 0      0 3.5  2.0  250 0   0      1 .57   .57   21    .049  .0041 - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 1 9.0 3.4 290 72 .15 0      -32 4.6  2.5  260 0   0      -32 42     26     2100   .62 0      0 4.6  2.6  250 0   0      1 .58   .58   21    .049  0      - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 9.0 3.6 300 77 .13 0      -32 4.4  2.4  260 0   0      1 8.2   5.1   310   .66 0      0 3.5  2.0  250 0   0      1 .57   .57   20    .049  0      - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 8.6 3.4 270 78 .12 0      -32 4.0  2.2  260 0   0      1 8.8   5.0   310   .62 0      0 3.4  2.0  250 0   0      1 .57   .59   20    .049  .0041 - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 9.7 3.7 300 80 .12 0      -32 4.0  2.2  260 0   0      1 9.9   5.5   310   .66 0      0 3.9  2.2  240 0   0      1 .57   .57   20    .049  0      - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 8.8 3.4 300 82 .13 0      -32 4.5  2.5  260 0   0      -32 8.4   4.6   310   .66 0      0 3.8  2.2  250 0   0      1 .59   .59   20    .045  0      - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 8.7 3.4 290 74 .13 0      -32 4.8  2.7  260 0   0      -32 7.6   4.5   290   .66 0      0 3.6  2.1  250 0   0      1 .58   .58   21    .045  0      - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 8.9 3.4 300 72 .13 0      -32 4.9  2.7  260 0   0      -32 6.8   4.2   300   .66 0      0 3.6  2.1  250 0   .0041 1 .57   .57   21    .045  .0041 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 0 9.5 3.5 200 72 .32 0      0 .59 .36 41 0   0      0 .020 .021 5.6 0    0      0 1.1  .74 47 0   0      0 .0016 .0020 .53 0      0      - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 8.9 3.3 300 67 .12 0      -32 4.9  2.6  260 0   0      1 11     6.0   310   .62 0      0 3.7  2.1  250 0   0      1 .61   .62   20    .045  0      - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 9.6 3.5 200 60 .32 0      0 .60 .37 40 0   0      0 .020 .020 5.6 0    0      0 .89 .59 46 0   0      0 .0019 .0044 .53 0      0      - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 0 9.6 3.5 200 73 .32 0      0 .65 .39 40 0   0      0 .025 .026 5.6 0    0      0 .94 .59 47 0   0      0 .0017 .0022 .53 0      0      - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 1 8.9 3.4 290 75 .13 0      -32 4.9  2.7  260 0   0      -32 7.0   4.4   290   .66 0      0 3.6  2.0  250 0   0      1 .57   .57   21    .049  0      - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 0 9.4 3.5 200 78 .32 0      0 .74 .45 41 0   0      0 .022 .025 5.6 0    0      0 1.0  .63 46 0   0      0 .0060 .0075 .54 0      0      - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 1 8.9 3.4 290 79 .14 0      -32 4.0  2.2  260 0   0      -32 6.7   4.2   300   .66 0      0 3.8  2.2  250 0   0      1 .58   .58   21    .049  .0041 - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 1 9.1 3.5 290 73 .12 0      -32 4.1  2.3  260 0   0      1 6.7   4.2   290   .66 0      0 3.4  1.9  250 0   0      1 .57   .57   20    .049  0      - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 8.4 3.3 290 73 .13 0      -32 4.0  2.2  260 0   0      -32 7.2   4.0   290   .66 0      0 4.3  2.4  250 0   0      1 .57   .57   20    .045  0      - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 8.9 3.4 300 67 .13 11      -32 4.0  2.2  260 0   0      -32 6.4   4.0   300   .66 0      0 3.7  2.1  250 0   0      1 .57   .57   20    .045  0      - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 8.6 3.5 310 82 .14 12      -32 4.8  2.6  260 0   0      -32 6.9   3.9   300   .66 0      0 3.4  2.0  250 0   0      1 .57   .57   21    .045  0      - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 0 9.4 3.4 200 66 .32 0      0 .58 .37 40 0   0      0 .021 .022 5.6 0    0      0 1.1  .66 47 0   0      0 .0053 .0064 .52 0      0      - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 8.7 3.3 300 85 .12 0      -32 4.3  2.4  260 0   0      1 7.2   4.6   310   .66 0      0 3.5  2.0  240 0   0      1 .56   .57   20    .045  0      - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 1 8.8 3.5 260 70 .12 0      -32 3.8  2.1  250 0   0      1 8.0   4.8   310   .66 .0041 0 3.6  2.0  250 0   0      1 .57   .57   20    .049  0      - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 12   6.4 430 100 160    0      - - - - 2 3.8  2.1  250 0   0      2 8.5   5.0   310   .66 0     
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 13   6.5 450 120 140    0      - - - - 2 4.4  2.4  250 0   0      2 6.7   3.8   310   .66 0     
recursive-simple/fibo_10_true-unreach-call_true-termination.c 2 65   36   4700 700 140    0      - - - - 0 3.3  1.9  250 0   0      2 36     23     2200   .62 .0041
recursive-simple/fibo_15_true-unreach-call.c 2 66   37   4800 680 140    52      - - - - 0 3.7  2.1  250 0   0      2 690     630     6400   .62 0     
recursive-simple/fibo_20_true-unreach-call.c 1 73   43   4700 840 150    .18   - - - - 0 4.5  2.5  250 0   0      0 960     920     5700   .63 0     
recursive-simple/fibo_25_true-unreach-call.c 0 9.8 3.5 200 70 .30 0      - - - - 0 .75 .46 40 0   0      0 .027 .028 5.6 0    0     
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 73   36   4600 750 140    13      - - - - 0 4.4  2.5  250 0   0      2 85     55     3200   .62 .0041
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 74   36   4700 700 140    0      - - - - 0 4.6  2.6  250 0   0      0 960     900     5400   .64 0     
recursive-simple/fibo_2calls_20_true-unreach-call.c 1 81   44   4800 800 150    .0041 - - - - 0 3.8  2.1  250 0   0      0 960     900     6200   .62 0     
recursive-simple/fibo_2calls_25_true-unreach-call.c 1 160   130   4700 1900 160    0      - - - - 0 3.6  2.0  250 0   0      0 960     890     6600   .63 0     
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 16   7.4 510 150 150    0      - - - - 2 4.3  2.4  250 0   0      2 13     7.6   390   .66 0     
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 23   9.3 640 190 140    0      - - - - 0 4.9  2.7  250 0   0      2 17     9.9   460   .66 0     
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 25   11   820 250 150    .0041 - - - - 0 4.2  2.3  250 0   0      2 22     14     510   .66 0     
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 33   13   970 270 140    0      - - - - 0 4.0  2.2  250 0   0      2 26     16     690   .66 0     
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 59   23   2100 530 140    0      - - - - 0 4.0  2.2  250 0   0      2 52     33     1000   .62 0     
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 22   9.1 760 180 140    0      - - - - 0 3.6  2.0  250 0   0      2 16     9.7   470   .66 0     
recursive-simple/fibo_7_true-unreach-call_true-termination.c 2 27   11   1100 250 140    .0082 - - - - 0 3.7  2.1  250 0   0      2 30     18     610   .66 0     
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 17   7.3 570 160 140    0      - - - - 0 4.1  2.3  250 0   0      2 13     8.0   450   .66 0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 18   7.7 650 160 140    0      - - - - 0 3.7  2.0  250 0   .0041 2 17     9.6   520   .66 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 18   7.9 660 150 140    0      - - - - 0 4.9  2.7  250 0   0      2 13     8.3   460   .62 0     
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 18   8.2 650 150 140    0      - - - - 0 3.4  1.9  250 0   0      2 15     8.9   510   .66 0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 16   7.1 510 120 150    0      - - - - 0 3.5  1.9  250 0   0      2 11     6.9   400   .66 0     
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 14   6.9 460 110 140    .0041 - - - - 0 4.1  2.3  250 0   0      2 8.2   4.7   310   .66 0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 15   6.8 460 130 150    0      - - - - 0 3.4  1.9  250 0   0      2 8.3   4.8   310   .66 0     
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 20   8.8 700 160 150    0      - - - - 0 3.3  1.9  250 0   0      2 17     10     480   .66 0     
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 25   11   820 220 150    0      - - - - 0 3.6  2.0  250 0   0      2 23     14     650   .66 0     
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 30   13   900 260 140    0      - - - - 0 3.5  2.0  250 0   0      2 38     23     560   .62 0     
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 0 9.5 3.4 200 70 .32 0      - - - - 0 .74 .45 41 0   0      0 .021 .021 5.6 0    0     
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 17   7.6 570 140 150    0      - - - - 0 3.4  1.9  250 0   0      2 14     8.5   440   .66 0     
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 21   9.7 720 180 150    0      - - - - 0 3.8  2.2  250 0   0      2 21     13     570   .62 0     
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 27   12   850 270 160    .0041 - - - - 0 4.3  2.4  250 0   0      2 28     17     510   .66 0     
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 34   16   950 310 140    0      - - - - 0 3.4  1.9  250 0   0      2 37     23     610   .66 0     
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 0 9.6 3.5 200 83 .32 0      - - - - 0 .68 .42 41 0   0      0 .020 .021 5.6 0    0     
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 15   7.2 470 120 140    0      - - - - 0 3.4  1.9  250 0   0      2 12     6.6   390   .66 0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 0 12   5.8 200 100 .32 0      - - - - 0 .64 .39 42 0   0      0 .020 .021 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 107 16000   15000   110000 140000 5500    90    44 -1152 490 290 25000 0   .18  44 -398 1100 680 56000 28   .0082 44 2 290   160   17000 0   .012 44 38 37 37 1400 1.8 .025 52 6 150 87   9900 0   .0082 52 64 6600 5900 59000 24 .0082
    correct results 70 102 7800   7000   69000 66000 4800    89    0 18 18 230 130 7300 12   .0041 2 2 7.2 4.1 490 0   0     38 38 36 36 1300 1.8 .025 3 6 12 6.9 750 0   0      32 64 1800 1400 29000 21 .0082
        correct true 32 64 3400   2900   41000 31000 4700    65    0 0 0 0 3 6 12 6.9 750 0   0      32 64 1800 1400 29000 21 .0082
        correct false 38 38 4300   4100   27000 34000 61    24    0 18 18 230 130 7300 12   .0041 2 2 7.2 4.1 490 0   0     38 38 36 36 1300 1.8 .025 0 0
    correct-unconfimed results 6 5 980   800   23000 8000 750    .18 0 0 0 0 0 0
        correct-unconfirmed true 5 5 970   800   23000 8000 750    .18 0 0 0 0 0 0
        correct-unconfirmed false 1 0 8.5 3.4 270 78 .13 0    0 0 0 0 0 0
    incorrect results 0 36 -1152 290 160 17000 0   .037 13 -416 130 78 5700 8.5 .0041 0 0 0 0
        incorrect true 0 36 -1152 290 160 17000 0   .037 13 -416 130 78 5700 8.5 .0041 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 107 -1152 -398 2 38 6 64
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Recursive