Tool PeSCo 1.7-svn b8d6131600+ 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] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 05:07:50 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 16 4.5 1200 120 0      0     1 4.4  2.5  260 0   0   1 8.1   4.5   310   .66 0   1 3.8  2.2  250 0      0   1 .58   .58   21    .049 0      - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 13 4.0 1200 95 0      0     1 4.5  2.5  260 0   0   1 7.7   4.4   300   .66 0   1 3.6  2.1  250 0      0   1 .58   .58   20    .049 .0041 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 1 14 3.8 1100 95 .012  0     -32 3.8  2.1  250 0   0   -32 6.4   4.1   290   .66 0   1 3.6  2.1  250 0      0   1 .57   .57   20    .049 0      - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 13 3.9 1100 99 .0082 0     1 4.4  2.5  250 0   0   1 7.3   4.1   300   .66 0   0 3.5  2.1  250 0      0   1 .58   .58   20    .049 0      - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 18 6.3 1300 160 .0082 .090 1 5.0  2.7  270 0   0   1 24     14     830   .62 0   1 4.0  2.3  250 0      0   1 .62   .63   21    .049 0      - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 1 31 19   1500 300 .0082 0     1 8.8  4.7  310 0   0   0 97     73     4200   1.6  0   1 5.2  2.8  270 0      0   1 .64   .64   23    .049 0      - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 12 3.7 1200 78 0      0     1 3.7  2.1  250 0   0   1 7.2   4.1   300   .66 0   1 3.8  2.2  250 0      0   1 .58   .58   20    .049 0      - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 2 14 4.5 1200 110 0      0     - - - - 0 4.0  2.2  250 0   0   2 18     11     470   .66 0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 900 870   3800 11000 0      0     - - - - 0 .77 .46 40 0   0   0 .026 .027 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 900 780   7000 11000 0      0     - - - - 0 .75 .45 41 0   0   0 .025 .026 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900 880   1800 13000 0      0     - - - - 0 .76 .47 40 0   0   0 .021 .022 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900 870   3600 12000 0      0     - - - - 0 4.0  2.3  250 0   0   2 420     330     2300   .62 0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900 860   11000 12000 .0082 0     - - - - 0 5.1  2.7  250 0   0   0 960     810     1400   .64 0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 910 890   2000 9700 .0082 0     - - - - 0 4.0  2.2  250 0   0   2 14     8.9   490   .62 0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 17 4.5 1300 130 0      0     - - - - 0 3.5  2.0  250 0   0   2 36     22     1400   .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 900 850   2400 13000 0      0     - - - - 0 .60 .38 40 0   0   0 .022 .023 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 15 4.3 1200 100 0      0     - - - - 0 3.4  1.9  250 0   0   2 9.8   6.0   330   .66 0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900 880   1800 14000 0      .033 - - - - 0 .68 .41 41 0   0   0 .021 .023 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900 870   2500 10000 0      0     - - - - 0 .59 .35 42 0   0   0 .021 .022 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 16 4.8 1300 130 .0082 .029 - - - - 0 3.5  2.0  250 0   0   2 11     6.6   360   .66 0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900 890   1600 14000 .0082 0     - - - - 0 3.7  2.1  250 0   0   0 960     820     960   .85 0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 1 15 4.2 1200 110 0      0     - - - - 0 4.9  2.7  250 0   0   0 960     890     6400   1.6  0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 900 870   2700 11000 0      0     - - - - 0 3.5  1.9  250 0   0   2 7.2   4.6   310   .66 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 910 870   5500 13000 0      0     - - - - 0 5.2  2.9  240 0   0   2 43     28     770   .66 0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 13 3.8 1100 91 .0082 0     -32 4.1  2.2  250 0   0   1 7.2   4.0   310   .66 0   1 3.7  2.2  250 0      0   1 .59   .59   20    .045 0      - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 11 3.5 1200 76 .0082 0     -32 3.7  2.1  250 0   0   1 8.6   4.9   310   .66 0   1 3.7  2.2  250 0      0   1 .56   .56   20    .045 0      - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 1 15 4.6 1300 110 0      0     1 11    5.6  450 0   0   0 96     63     5500   1.4  0   1 6.5  3.6  280 0      0   1 .70   .70   27    .049 0      - -
recursive-simple/fibo_15_false-unreach-call.c 1 30 13   2200 280 0      0     1 58    35    2100 0   0   0 97     63     6700   .79 0   1 32    16    1300 0      0   1 2.1    2.1    99    .049 0      - -
recursive-simple/fibo_20_false-unreach-call.c 1 380 340   11000 3500 0      0     0 98    52    4300 0   0   0 87     57     7000   1.5  0   0 97    51    4500 .84   0   1 19      19      940    .049 0      - -
recursive-simple/fibo_25_false-unreach-call.c 0 220 110   15000 1900 0      0     0 .64 .39 41 0   0   0 .022 .023 5.8 0    0   0 .95 .61 47 0      0   0 .0021 .0027 .40 0     0      - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 17 4.9 1300 130 0      0     1 11    5.8  430 0   0   0 97     65     6100   1.5  0   1 8.1  4.3  330 0      0   1 .72   .72   27    .049 0      - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 31 12   2100 260 0      0     1 55    33    2100 0   0   0 78     48     7000   1.7  0   1 24    13    1100 0      0   1 2.1    2.1    99    .049 0      - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 1 440 410   11000 4400 0      0     0 98    51    4300 0   0   0 83     51     7000   .72 0   0 98    52    4300 1.6    0   1 19      19      940    .049 0      - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 240 120   15000 2300 0      0     0 .61 .37 40 0   0   0 .024 .025 5.6 0    0   0 .97 .61 48 0      0   0 .0016 .0020 .53 0     0      - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 12 3.6 1200 78 .012  0     1 4.3  2.4  250 0   0   1 7.5   4.7   310   .62 0   1 3.7  2.1  250 0      0   1 .60   .60   20    .049 0      - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 14 4.1 1100 100 0      0     1 5.3  2.9  270 0   0   1 8.8   4.8   320   .62 0   1 4.5  2.6  250 0      0   1 .61   .61   21    .049 0      - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 15 4.2 1200 100 0      0     1 6.2  3.4  270 0   0   0 97     65     6900   .96 0   1 4.2  2.4  250 0      0   1 .59   .59   21    .049 0      - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 15 4.3 1200 110 0      0     1 5.4  3.0  280 0   0   1 63     38     2500   .62 0   1 4.2  2.4  260 0      0   1 .60   .60   21    .049 0      - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 1 15 4.4 1200 110 0      0     1 8.0  4.4  300 0   0   0 97     70     4300   1.7  0   1 5.4  3.0  290 0      0   1 .64   .64   23    .049 0      - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 15 4.1 1200 110 0      0     1 5.3  2.9  270 0   0   1 25     14     940   .62 0   1 3.8  2.2  250 0      0   1 .59   .59   21    .049 0      - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 1 15 4.2 1200 110 0      0     1 6.5  3.5  290 0   0   0 97     71     3700   1.1  0   1 5.0  2.8  280 0      0   1 .61   .61   22    .049 0      - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 14 4.1 1100 110 0      0     1 4.2  2.3  260 0   0   1 7.8   4.7   300   .66 0   1 3.6  2.1  250 0      0   1 .58   .58   20    .049 0      - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 15 4.1 1200 92 0      0     1 4.4  2.5  260 0   0   1 7.5   4.7   310   .62 0   1 3.5  2.1  250 0      0   1 .57   .57   21    .049 0      - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 12 3.8 1200 98 0      0     1 4.4  2.5  260 0   0   1 8.1   4.5   310   .62 0   1 3.5  2.1  250 0      0   1 .61   .61   20    .049 0      - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 14 4.0 1200 95 0      0     1 4.9  2.7  260 0   0   1 9.3   5.4   350   .66 0   1 4.0  2.3  250 0      0   1 .57   .57   21    .045 0      - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 13 4.0 1200 91 0      0     1 5.8  3.2  270 0   0   1 13     7.0   540   .62 0   1 4.1  2.4  250 0      0   1 .58   .58   21    .045 0      - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 14 4.2 1200 100 0      0     1 6.0  3.3  270 0   0   1 15     8.4   740   .62 0   1 5.1  2.9  250 0      0   1 .59   .59   21    .045 0      - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 14 4.1 1200 85 0      0     1 6.7  3.6  280 0   0   1 20     12     890   .66 0   1 4.8  2.8  270 0      0   1 .58   .58   21    .045 0      - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 12 3.8 1200 100 0      0     1 4.8  2.7  260 0   0   1 7.5   4.2   290   .62 0   1 3.7  2.1  250 0      0   1 .59   .59   20    .045 .0041 - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 1 150 100   3700 1500 0      0     0 13    6.5  440 0   0   0 98     65     6000   1.5  0   0 11    130    400 .0041 0   1 1.1    1.1    47    .049 0      - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 1 16 4.8 1300 120 0      0     1 16    8.4  550 0   0   0 97     63     6400   1.6  0   1 9.2  4.9  420 0      0   1 .64   .64   23    .049 0      - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 1 15 4.3 1200 94 0      0     1 5.3  2.9  270 0   0   1 9.5   5.2   370   .66 0   1 3.9  2.2  250 0      0   1 .60   .60   21    .049 0      - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 1 23 6.6 1400 160 0      0     1 38    24    1400 0   0   0 98     68     6300   1.5  0   1 16    8.8  630 0      0   1 .70   .70   26    .049 0      - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 1 15 4.3 1200 100 0      0     1 6.0  3.3  280 0   0   1 15     8.3   730   .62 0   1 5.2  3.0  260 0      0   1 .63   .63   21    .049 0      - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 1 14 4.1 1200 100 0      0     1 4.2  2.4  260 0   0   1 7.7   4.7   300   .66 0   1 3.6  2.1  250 0      0   1 .57   .57   20    .049 .0041 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 14 4.1 1100 110 0      0     1 5.0  2.7  270 0   0   1 9.7   5.4   330   .62 0   1 4.0  2.2  250 0      0   1 .60   .59   21    .045 .0041 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 13 3.9 1200 100 0      0     1 5.6  3.0  270 0   0   1 11     6.6   520   .66 0   1 4.2  2.4  250 0      0   1 .58   .58   21    .045 0      - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 14 4.1 1200 110 0      0     1 6.7  3.6  280 0   0   1 14     8.1   630   .62 0   1 4.5  2.5  250 0      0   1 .57   .57   21    .045 0      - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 13 4.0 1200 98 0      0     1 6.5  3.5  280 0   0   1 18     10     690   .62 0   1 4.5  2.5  260 0      0   1 .58   .58   21    .045 0      - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 14 3.9 1100 92 0      0     1 4.3  2.4  260 0   0   1 7.0   4.4   300   .66 0   1 3.7  2.1  250 0      0   1 .56   .57   21    .045 0      - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 1 13 3.9 1100 100 .0082 0     1 3.8  2.1  250 0   0   1 7.5   4.7   310   .62 0   0 3.6  2.1  250 0      0   1 .57   .57   20    .049 0      - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 13 3.6 1000 78 0      0     - - - - 2 4.3  2.4  250 0   0   2 7.9   4.9   310   .62 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 11 3.5 1200 80 0      0     - - - - 2 3.4  1.9  250 0   0   2 8.6   4.8   310   .66 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c 2 17 4.7 1300 120 0      0     - - - - 0 4.5  2.5  250 0   0   2 51     32     3000   .62 0  
recursive-simple/fibo_15_true-unreach-call.c 2 46 30   1700 480 0      0     - - - - 0 4.2  2.4  250 0   0   2 710     640     6400   .62 0  
recursive-simple/fibo_20_true-unreach-call.c 0 920 880   2200 11000 0      0     - - - - 0 3.7  2.1  250 0   0   0 880     840     7000   .66 0  
recursive-simple/fibo_25_true-unreach-call.c 0 960 870   5400 12000 0      0     - - - - 0 .78 .49 44 0   0   0 5.3   3.3   270   .65 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 18 5.0 1300 150 0      0     - - - - 0 4.5  2.5  250 0   0   2 98     62     3500   .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 59 43   1700 690 0      0     - - - - 0 4.3  2.5  250 0   0   0 960     900     5500   .65 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 920 880   2200 14000 0      0     - - - - 0 3.6  2.0  250 0   0   0 960     910     5200   .66 0  
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 960 860   5500 13000 0      0     - - - - 0 .65 .39 42 0   0   0 5.1   2.8   260   .65 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 11 3.6 1200 96 0      0     - - - - 2 4.2  2.4  250 0   0   2 14     8.3   390   .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 15 4.1 1200 97 0      0     - - - - 0 4.6  2.6  250 0   0   2 17     10     550   .66 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 14 4.1 1200 97 0      0     - - - - 0 4.0  2.2  250 0   0   2 29     17     630   .66 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 15 4.2 1200 110 0      0     - - - - 0 4.4  2.5  250 0   0   2 33     20     590   .66 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 14 4.2 1300 100 0      0     - - - - 0 4.7  2.6  250 0   0   2 49     30     1100   .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 15 4.2 1200 100 0      0     - - - - 0 4.4  2.5  250 0   0   2 16     9.5   510   .66 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c 2 15 4.2 1200 98 0      0     - - - - 0 3.5  1.9  250 0   0   2 23     14     770   .66 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 14 4.0 1100 98 0      0     - - - - 0 4.4  2.4  250 0   0   2 13     7.6   450   .66 0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 12 3.9 1200 90 0      0     - - - - 0 3.9  2.2  250 0   0   2 15     9.2   510   .66 0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 14 4.0 1100 110 0      0     - - - - 0 4.8  2.7  250 0   0   2 16     9.5   510   .66 0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 14 4.1 1100 86 0      0     - - - - 0 3.6  2.0  240 0   0   2 15     8.9   510   .66 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 14 4.0 1100 94 0      0     - - - - 0 3.5  2.0  250 0   0   2 13     8.0   380   .66 0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 14 3.9 1100 100 0      0     - - - - 0 3.9  2.2  250 0   0   2 8.5   5.3   320   .62 0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 13 3.8 1200 91 0      0     - - - - 0 3.9  2.2  250 0   0   2 8.5   5.3   310   .66 0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 14 4.1 1100 100 0      0     - - - - 0 4.0  2.2  250 0   0   2 19     11     520   .66 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 13 3.9 1200 110 0      0     - - - - 0 4.4  2.5  250 0   0   2 27     16     660   .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 15 4.1 1200 99 0      0     - - - - 0 3.5  2.0  250 0   0   2 29     18     710   .62 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 15 4.1 1200 110 0      0     - - - - 0 4.3  2.4  250 0   0   2 42     26     620   .66 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 12 3.8 1200 88 0      0     - - - - 0 4.3  2.4  250 0   0   2 12     7.2   430   .66 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 14 4.1 1100 91 0      0     - - - - 0 4.1  2.2  250 0   0   2 20     12     600   .66 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 14 4.2 1200 97 0      0     - - - - 0 4.0  2.2  250 0   0   2 26     16     650   .66 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 15 4.3 1200 120 0      0     - - - - 0 4.6  2.6  250 0   0   2 45     28     590   .62 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 15 4.3 1200 120 0      0     - - - - 0 4.8  2.7  250 0   0   2 55     36     880   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 14 4.0 1100 87 0      0     - - - - 0 4.4  2.4  250 0   0   2 11     6.5   390   .66 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 14 4.3 1200 96 .0082 0     - - - - 0 4.5  2.5  260 0   0   2 10     5.8   340   .66 0  
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 96 112 17000 15000 210000 220000 .11  .15  44 -60 570 320   25000 0   0   44 -4 1600   1000   92000 36    0   44 37 440 360 22000 2.4 0   44 42 65 65 2900 2.0 .016 52 6 190 100   11000 0   0   52 76 7700 6700 61000 31 0  
    correct results 76 110 2100 1200 110000 18000 .090 .12  36 36 350 200   15000 0   0   28 28 360   210   15000 18    0   37 37 220 120 12000 0   0   42 42 65 65 2900 2.0 .016 3 6 12 6.7 750 0   0   38 76 2000 1500 34000 24 0  
        correct true 34 68 520 170 41000 3900 .016 .029 0 0 0 0 3 6 12 6.7 750 0   0   38 76 2000 1500 34000 24 0  
        correct false 42 42 1600 1000 73000 14000 .074 .090 36 36 350 200   15000 0   0   28 28 360   210   15000 18    0   37 37 220 120 12000 0   0   42 42 65 65 2900 2.0 .016 0 0
    correct-unconfimed results 2 2 74 47 2900 810 0     0     0 0 0 0 0 0
        correct-unconfirmed true 2 2 74 47 2900 810 0     0     0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 3 -96 12 6.4 750 0   0   1 -32 6.4 4.1 290 .66 0   0 0 0 0
        incorrect true 0 3 -96 12 6.4 750 0   0   1 -32 6.4 4.1 290 .66 0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 112 -60 -4 37 42 6 76
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Recursive