Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 22:46:12 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options --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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 .25 .24 17 2.6 0     0      1 9.5 5.2 300 0   0      -32 7.0 3.9 310 .62 0   1 3.5 2.0 250 0   0      1 .60 .60 20 .049 .0041 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 .24 .23 18 2.9 0     0      1 5.0 2.8 270 0   .15   -32 7.3 4.1 310 .62 0   1 3.5 2.1 250 0   0      1 .57 .57 20 .049 .0041 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 1 .19 .19 17 2.2 0     0      1 3.9 2.2 250 0   0      -32 7.1 3.9 300 .62 0   1 3.5 2.1 250 0   0      1 .59 .59 20 .049 0      - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 .26 .25 17 3.2 0     0      1 4.0 2.2 250 0   0      -32 7.0 4.0 300 .62 0   1 3.4 2.0 250 0   0      1 .58 .58 20 .049 0      - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 .36 .36 18 4.9 0     0      1 15   8.3 450 0   0      -32 6.7 3.8 300 .62 0   1 3.4 2.0 250 0   0      1 .59 .59 20 .049 0      - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 1 .55 .55 17 6.4 0     0      0 13   7.4 430 0   .074  -32 6.9 3.9 300 .62 0   1 3.5 2.0 250 0   0      1 .57 .57 20 .049 0      - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 .23 .23 18 2.7 0     0      1 3.7 2.1 250 0   0      -32 6.9 3.8 300 .62 0   1 3.3 1.9 250 0   .0041 1 .64 .68 20 .049 0      - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 830    840    15000 12000   .045 0      - - - - 0 .63 .39 41 0   0     0 .025 .026 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 830    840    15000 12000   .045 0      - - - - 0 .76 .47 40 0   0     0 .025 .027 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 900    900    15000 15000   .053 .0041 - - - - 0 .75 .46 41 0   0     0 .021 .021 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    67 9000   .016 0      - - - - 0 .74 .47 40 0   0     0 .022 .023 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    96 8700   .012 0      - - - - 0 .71 .43 41 0   0     0 .027 .027 5.6 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    1500 12000   .025 0      - - - - 0 .70 .42 41 0   0     0 .021 .022 5.7 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 590    600    15000 9600   .053 0      - - - - 0 .68 .41 40 0   0     0 .021 .022 5.7 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 .14 .14 15 1.4 0     0      - - - - 0 3.7  2.1  250 0   0     2 31     19     1300   .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 540    540    15000 7300   .037 0      - - - - 0 .71 .43 41 0   0     0 .021 .022 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    260 14000   .025 0      - - - - 0 .59 .35 40 0   0     0 .025 .026 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    45 11000   .020 0      - - - - 0 .68 .43 42 0   0     0 .027 .028 5.7 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900    900    1000 12000   .025 0      - - - - 0 .70 .44 41 0   0     0 .023 .023 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    59 11000   .012 0      - - - - 0 .69 .42 40 0   0     0 .021 .021 5.8 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    73 13000   .012 0      - - - - 0 .69 .42 42 0   0     0 .021 .022 5.7 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 650    660    15000 9800   .049 0      - - - - 0 .79 .48 42 0   0     0 .021 .022 5.7 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2 .41 .41 17 4.6 0     0      - - - - 0 3.9  2.2  250 0   .029 2 9.0   5.1   310   .66 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 2 .40 .40 18 5.5 0     0      - - - - 0 3.8  2.1  250 0   0     2 12     7.6   510   .66 0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 .16 .16 16 2.3 0     0      1 4.4 2.5 250 0   0      -32 7.0 3.9 300 .62 0   1 3.4 2.0 250 0   0      1 .58 .58 20 .045 0      - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 .17 .16 15 1.8 0     0      1 3.5 2.0 250 0   .0041 -32 6.5 3.7 290 .66 0   1 3.3 2.0 240 0   0      1 .57 .57 20 .045 0      - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 1 .17 .16 16 2.3 0     0      1 6.9 3.9 330 0   0      -32 6.4 3.7 290 .62 0   1 3.4 2.0 250 0   0      1 .58 .58 20 .049 0      - -
recursive-simple/fibo_15_false-unreach-call.c 1 .18 .18 18 2.4 0     0      1 21   14   1200 0   0      -32 6.7 3.9 310 .62 0   1 3.5 2.0 240 0   .0041 1 .57 .57 20 .049 0      - -
recursive-simple/fibo_20_false-unreach-call.c 1 .33 .32 46 5.0 0     0      0 41   32   7000 0   0      -32 6.5 4.1 300 .62 0   1 4.4 2.5 250 0   .0041 1 .57 .57 20 .049 0      - -
recursive-simple/fibo_25_false-unreach-call.c 1 2.0  2.0  370 32   0     0      0 97   64   4000 0   0      -32 6.8 4.3 300 .62 0   1 3.3 2.0 250 0   0      1 .59 .59 20 .049 0      - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 .18 .18 16 2.1 0     0      1 6.9 4.0 380 0   13      -32 7.1 4.0 300 .62 0   1 3.6 2.1 250 0   0      1 .58 .60 20 .049 0      - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 .20 .20 18 2.2 0     0      1 22   15   1200 0   0      -32 7.3 4.1 300 .62 0   1 3.4 2.0 250 0   0      1 .58 .58 20 .049 0      - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 1 .35 .35 48 5.3 0     0      0 51   37   7000 0   .029  -32 7.0 4.0 300 .62 0   1 3.5 2.1 250 0   0      1 .58 .58 20 .049 0      - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 1 2.1  2.1  390 29   0     0      0 98   59   3500 0   .029  -32 6.5 4.1 300 .62 0   1 3.4 2.0 250 0   0      1 .57 .57 20 .049 0      - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 .17 .16 16 1.9 0     .28   1 3.9 2.1 250 0   0      -32 6.7 4.2 310 .62 0   1 3.5 2.1 240 0   0      1 .57 .57 20 .049 0      - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 .17 .17 15 2.0 0     0      1 4.5 2.4 260 0   0      -32 7.0 3.9 300 .62 0   1 3.5 2.1 250 0   0      1 .58 .61 20 .049 0      - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 .16 .16 16 2.2 0     0      1 4.8 2.7 270 0   0      -32 6.8 4.3 300 .62 0   1 4.0 2.3 240 0   0      1 .57 .57 20 .049 0      - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 .17 .16 16 2.0 0     0      1 5.2 2.9 270 0   0      -32 7.1 3.9 300 .62 0   1 3.5 2.0 250 0   0      1 .58 .57 20 .049 0      - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 1 .16 .16 15 1.9 0     0      1 6.7 3.7 290 0   0      -32 6.9 4.0 300 .62 0   1 3.5 2.0 250 0   0      1 .60 .60 20 .049 0      - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 .19 .19 16 1.8 0     0      1 5.2 2.8 270 0   0      -32 7.0 3.9 310 .62 0   1 3.3 1.9 250 0   0      1 .61 .61 20 .049 0      - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 1 .17 .17 16 1.9 0     0      1 4.9 2.7 280 0   0      -32 6.8 4.2 300 .62 0   1 3.5 2.0 240 0   0      1 .58 .58 20 .049 0      - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 .24 .23 18 3.1 0     0      1 4.5 2.5 260 0   0      -32 7.5 4.1 300 .62 0   1 3.5 2.1 250 0   0      1 .56 .56 20 .049 0      - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 .16 .16 15 2.0 0     0      1 4.3 2.4 260 0   0      -32 6.8 3.9 300 .62 0   1 4.5 2.6 250 0   0      1 .58 .58 20 .049 0      - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 1 .22 .21 18 2.6 0     0      1 4.2 2.3 260 0   0      -32 6.4 4.1 300 .62 0   1 4.4 2.5 250 0   .26   1 .60 .63 20 .049 0      - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 .16 .16 16 1.9 0     0      1 4.5 2.5 260 0   0      -32 6.2 3.6 300 .62 0   1 3.4 2.0 240 0   0      1 .57 .57 20 .045 0      - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 .16 .16 15 1.7 0     0      1 6.3 3.5 270 0   .14   -32 6.9 3.8 300 .62 0   1 3.5 2.1 250 0   0      1 .62 .61 20 .045 0      - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 .18 .18 16 1.8 0     0      1 4.6 2.5 270 0   0      -32 6.4 4.0 290 .62 0   1 3.5 2.1 250 0   .0041 1 .60 .61 20 .045 0      - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 .18 .17 16 1.7 0     0      1 5.0 2.7 270 0   0      -32 6.6 3.7 300 .62 0   1 3.4 2.0 250 0   .0041 1 .58 .58 20 .045 0      - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 .16 .16 17 2.1 0     0      1 4.2 2.3 260 0   0      -32 6.7 4.2 300 .62 0   1 3.5 2.0 250 0   0      1 .58 .58 20 .045 0      - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 1 .21 .21 18 2.0 0     0      0 98   78   2400 0   0      -32 6.7 3.8 290 .62 0   1 4.0 2.3 250 0   0      1 .61 .60 20 .049 0      - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 1 .19 .18 17 2.2 0     0      1 17   8.8 640 0   0      -32 6.5 3.7 300 .62 0   1 3.4 2.0 250 0   0      1 .59 .59 20 .049 0      - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 1 .19 .19 17 2.0 0     .28   1 4.9 2.7 270 0   0      -32 6.5 3.7 290 .62 0   1 3.5 2.0 250 0   0      1 .57 .57 20 .049 0      - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 1 .19 .18 17 2.0 0     0      1 28   17   1600 0   0      -32 6.8 4.2 300 .62 0   1 3.8 2.2 250 0   0      1 .57 .57 20 .049 .0041 - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 1 .19 .18 17 2.5 0     0      1 5.9 3.2 270 0   0      -32 7.1 3.9 300 .62 0   1 3.5 2.0 250 0   0      1 .58 .58 20 .049 0      - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 1 .19 .18 18 2.3 0     .28   1 4.7 2.6 260 0   0      -32 6.5 3.7 300 .62 0   1 3.4 2.0 240 0   0      1 .57 .57 20 .049 .0041 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 .16 .16 15 2.0 0     0      1 5.9 3.3 260 0   0      -32 6.3 3.6 290 .62 0   1 3.5 2.0 240 0   0      1 .56 .56 20 .045 0      - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 .17 .17 17 1.7 0     0      1 4.9 2.7 270 0   .074  -32 7.1 4.0 320 .62 0   1 3.6 2.1 250 0   0      1 .56 .56 20 .045 0      - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 .16 .16 15 1.9 0     0      1 4.7 2.6 270 0   0      -32 6.5 4.2 300 .66 0   1 3.4 2.0 250 0   0      1 .58 .58 20 .045 0      - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 .19 .19 16 1.8 0     0      1 6.2 3.4 280 0   0      -32 6.7 4.2 300 .62 0   1 3.6 2.1 250 0   0      1 .56 .56 20 .045 0      - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 .16 .16 16 1.8 0     0      1 4.5 2.5 260 0   .012  -32 6.6 4.2 290 .62 0   1 4.1 2.4 250 0   0      1 .57 .57 20 .045 0      - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 1 .18 .18 16 2.1 0     0      1 3.7 2.0 250 0   0      -32 7.1 4.0 310 .62 0   1 3.6 2.1 250 0   0      1 .57 .57 20 .049 0      - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 .14 .13 15 1.6 0     0      - - - - 2 3.6  2.1  250 0   0     2 8.5   5.1   310   .66 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 .14 .14 16 1.7 0     0      - - - - 2 3.6  2.0  250 0   0     2 7.3   4.2   310   .62 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c 2 .14 .14 16 1.7 0     0      - - - - 0 3.7  2.1  250 0   0     2 41     25     2300   .62 0  
recursive-simple/fibo_15_true-unreach-call.c 1 .15 .14 15 1.5 0     0      - - - - 0 4.5  2.5  250 0   0     0 960     920     4900   .63 0  
recursive-simple/fibo_20_true-unreach-call.c 1 .21 .20 19 2.4 0     0      - - - - 0 4.0  2.2  250 0   0     0 960     900     6200   .64 0  
recursive-simple/fibo_25_true-unreach-call.c 1 .90 .90 80 14   0     0      - - - - 0 3.6  2.0  250 0   0     0 960     910     4700   1.4  0  
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 .14 .14 15 1.7 0     .28   - - - - 0 4.4  2.5  250 0   0     2 90     60     4000   .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 .15 .14 15 1.9 0     0      - - - - 0 4.5  2.6  250 0   0     0 960     900     5400   .67 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c 1 .21 .21 19 2.7 0     0      - - - - 0 4.5  2.5  250 0   0     0 960     910     5600   .64 0  
recursive-simple/fibo_2calls_25_true-unreach-call.c 1 .93 .93 83 13   0     0      - - - - 0 4.0  2.3  250 0   0     0 620     570     7000   .64 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 .14 .13 15 1.7 0     0      - - - - 2 3.5  2.0  250 0   0     2 12     7.2   390   .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 .15 .15 15 1.6 0     0      - - - - 0 4.4  2.4  250 0   0     2 17     10     540   .62 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 .15 .14 16 1.5 0     0      - - - - 0 3.8  2.1  250 0   0     2 27     16     650   .66 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 .14 .14 16 1.5 0     0      - - - - 0 4.3  2.4  250 0   0     2 32     19     710   .62 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 .16 .15 16 1.5 0     0      - - - - 0 4.1  2.3  250 0   0     2 58     36     1200   .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 .16 .16 16 1.6 0     0      - - - - 0 4.2  2.4  250 0   0     2 18     11     590   .66 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c 2 .14 .13 16 1.7 0     .28   - - - - 0 3.5  2.0  250 0   0     2 23     14     660   .62 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    850 11000   .025 0      - - - - 0 .63 .38 42 0   0     0 .028 .029 5.6 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    860 12000   .025 0      - - - - 0 .59 .36 40 0   0     0 .027 .027 5.5 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    860 12000   .025 0      - - - - 0 .65 .39 43 0   0     0 .022 .022 5.6 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 .16 .16 16 1.8 0     0      - - - - 0 4.0  2.2  250 0   0     2 14     8.6   470   .62 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1800 11000   .025 0      - - - - 0 .78 .47 41 0   0     0 .027 .028 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1800 12000   .025 0      - - - - 0 .59 .35 41 0   0     0 .021 .022 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1800 10000   .025 0      - - - - 0 .62 .40 40 0   0     0 .021 .021 5.6 0    0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 .15 .15 15 1.6 0     0      - - - - 0 4.1  2.3  250 0   0     2 20     12     530   .62 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 .14 .14 15 1.7 0     0      - - - - 0 3.5  2.0  250 0   0     2 28     16     670   .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 .14 .13 15 1.6 0     0      - - - - 0 4.4  2.5  250 0   0     2 32     20     700   .62 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 .14 .13 16 1.4 0     0      - - - - 0 4.1  2.3  250 0   0     2 37     24     800   .66 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 .13 .13 16 1.7 0     0      - - - - 0 4.2  2.4  250 0   0     2 12     7.2   440   .66 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 .14 .14 15 1.7 0     0      - - - - 0 3.8  2.1  250 0   0     2 19     12     580   .66 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 .17 .18 20 1.4 0     5.2    - - - - 0 4.3  2.4  250 0   0     2 28     17     640   .62 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 .14 .14 15 1.5 0     0      - - - - 0 4.1  2.3  250 0   0     2 42     27     700   .66 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 .16 .16 15 1.4 0     0      - - - - 0 3.6  2.0  250 0   0     2 64     42     820   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 .16 .16 16 1.7 0     .41   - - - - 0 3.6  2.0  250 0   0     2 12     6.8   390   .62 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 .15 .14 15 1.6 0     0      - - - - 0 4.0  2.3  250 0   0     2 12     6.7   330   .62 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 102 17000   17000   100000 220000 .58 7.0  44 38 670 430 38000 0   13 44 -1408 300 170 13000 27 0   44 44 160 92 11000 0   .28 44 44 26 26 890 2.1 .016 52 6 140 80   8800 0   .029 52 52 6100 5500 55000 21 0  
    correct results 70 96 17   17   1900 210 0    7.0  38 38 270 150 14000 0   13 0 44 44 160 92 11000 0   .28 44 44 26 26 890 2.1 .016 3 6 11 6.0 750 0   0     26 52 710 440 21000 17 0  
        correct true 26 52 4.3 4.3 410 48 0    6.2  0 0 0 0 3 6 11 6.0 750 0   0     26 52 710 440 21000 17 0  
        correct false 44 44 13   13   1500 160 0    .84 38 38 270 150 14000 0   13 0 44 44 160 92 11000 0   .28 44 44 26 26 890 2.1 .016 0 0
    correct-unconfimed results 6 6 2.5 2.5 230 35 0    0    0 0 0 0 0 0
        correct-unconfirmed true 6 6 2.5 2.5 230 35 0    0    0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 0 44 -1408 300 170 13000 27 0   0 0 0 0
        incorrect true 0 0 44 -1408 300 170 13000 27 0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 102 38 -1408 44 44 6 52
Run set symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Recursive